normedAddCommGroup — Mathlib

English

The spectral norm equips L with the structure of a normed additive commutative group.

Русский

Спектральная норма наделяет L структурой нормированной аддитивной коммутативной группы.

LaTeX

$$$\text{NormedAddCommGroup}(L)$$$

Lean4

/-- `L` with the spectral norm is a `normed_add_comm_group`. -/
def normedAddCommGroup [CompleteSpace K] : NormedAddCommGroup L :=
  by
  haveI : NormedField L := normedField K L
  infer_instance

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