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.
Equivs #In this file, we transfer a normed field structure across an equivalence.
This continues the pattern set in Mathlib/Algebra/Module/TransferInstance.lean.