Transfer normed algebraic structures across Equivs #
In this file, we transfer a (semi-)normed ring structure across an equivalence.
This continues the pattern set in Mathlib/Algebra/Module/TransferInstance.lean.
@[reducible, inline]
Transfer a SeminormedRing across an Equiv
Equations
Instances For
@[reducible, inline]
abbrev
Equiv.normedRing
{α : Type u_1}
{β : Type u_2}
[NormedRing β]
(e : α ≃ β)
:
NormedRing α
Transfer a NormedRing across an Equiv