Transfer algebraic structures across Equiv
s #
This continues the pattern set in Mathlib/Algebra/Group/TransferInstance.lean
.
@[reducible, inline]
Transfer DivisionRing
across an Equiv
Equiv
s #This continues the pattern set in Mathlib/Algebra/Group/TransferInstance.lean
.
Transfer DivisionRing
across an Equiv