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]

abbrev Equiv.seminormedRing {α : Type u_1} {β : Type u_2} [SeminormedRing β] (e : α ≃ β) : SeminormedRing α

Transfer a SeminormedRing across an Equiv

Equations

• e.seminormedRing = SeminormedRing.induced α β e.ringEquiv

@[reducible, inline]

abbrev Equiv.normedRing {α : Type u_1} {β : Type u_2} [NormedRing β] (e : α ≃ β) : NormedRing α

Transfer a NormedRing across an Equiv

Equations

• e.normedRing = NormedRing.induced α β e.ringEquiv ⋯