Transfer normed algebraic structures across Equivs

In this file, we transfer a normed field structure across an equivalence. This continues the pattern set in Mathlib/Algebra/Module/TransferInstance.lean.

@[reducible, inline]

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

Transfer a NormedField across an Equiv

Equations

• e.normedField = NormedField.induced α β e.ringEquiv ⋯