spectralMulAlgNorm — Mathlib

English

The spectral norm yields a multiplicative K-algebra norm on L, i.e., a norm that respects multiplication and the K-algebra structure.

Русский

Спектральная норма образует мультипликативную K-алгебраическую норму на L, сохраняющую умножение и структуру K-алгебры.

LaTeX

$$$\text{spectralMulAlgNorm} = \text{spectralAlgNorm}$ with $\text{map_one'}$ and $\text{map_mul'}$ as in the standard construction$$

Lean4

/-- The spectral norm is a multiplicative `K`-algebra norm on `L`. -/
def spectralMulAlgNorm [CompleteSpace K] : MulAlgebraNorm K L :=
  { spectralAlgNorm K L with
    map_one' := spectralAlgNorm_one
    map_mul' := spectralAlgNorm_mul }

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