normedAddCommGroupProdAux — Mathlib

English

There is a canonical NormedAddCommGroup structure on the product C⋆ᵐᵒᵈ(A, E×F).

Русский

Существует каноническая структура NormedAddCommGroup на произведении C⋆ᵐᵒᵈ(A, E×F).

LaTeX

$$$\\text{instNormedAddCommGroupProd}:= \\text{NormedAddCommGroup on } C⋆ᵐᵒᵈ(A, E\\times F)$$$

Lean4

/-- A normed additive commutative group structure on `C⋆ᵐᵒᵈ(A, E × F)` with the wrong topology,
uniformity and bornology. This is only used to build the instance with the correct forgetful
inheritance data. -/
noncomputable def normedAddCommGroupProdAux : NormedAddCommGroup C⋆ᵐᵒᵈ(A, E × F) :=
  NormedAddCommGroup.ofCore (CStarModule.normedSpaceCore A)

Похожие утверждения