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