Transfer normed algebraic structures across Equivs or AddEquivs

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 AddEquiv.normedSpace {α : Type u_1} {β : Type u_2} (𝕜 : Type u_3) [NormedField 𝕜] [AddCommGroup α] [SeminormedAddCommGroup β] [NormedSpace 𝕜 β] (e : α ≃+ β) : NormedSpace 𝕜 α

Transfer NormedSpace across an AddEquiv

Equations

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

@[deprecated AddEquiv.normedSpace (since := "2026-07-30")]

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

Alias of AddEquiv.normedSpace.

---

Transfer NormedSpace across an AddEquiv

Equations

• @Equiv.normedSpace = @AddEquiv.normedSpace