Transfer normed algebraic structures across Equivs

In this file, we transfer a (semi-)normed (additive) commutative group and normed space structures across an equivalence. This continues the pattern set in Mathlib/Algebra/Module/TransferInstance.lean.

@[reducible, inline]

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

Transfer a SeminormedCommGroup across an Equiv

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

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

Transfer a SeminormedAddCommGroup across an Equiv

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

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

Transfer a NormedCommGroup across an Equiv

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

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

Transfer a NormedAddCommGroup across an Equiv

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Equiv.normedSpace {α : Type u_1} {β : Type u_2} (𝕜 : Type u_3) [NormedField 𝕜] [SeminormedAddCommGroup β] [NormedSpace 𝕜 β] (e : α ≃ β) : NormedSpace 𝕜 α

Transfer NormedSpace across an Equiv

Equations

• Equiv.normedSpace 𝕜 e = NormedSpace.induced 𝕜 α β (Equiv.linearEquiv 𝕜 e)