nnnorm_def — Mathlib

English

The pair of Normed Ring and Normed Space structures together give a Normed Algebra structure on 𝓜(𝕜,A).

Русский

Сочетание структур нормированного кольца и нормированного пространства образует нормированную алгебру на 𝓜(𝕜,A).

LaTeX

$$$\text{NormedAlgebra}(\mathcal{M}(\mathbb{K},A))$$$

Lean4

theorem nnnorm_def (a : 𝓜(𝕜, A)) : ‖a‖₊ = ‖toProdHom a‖₊ :=
  rfl

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