normedAlgebra — Mathlib

English

The product of finitely many normed algebras is a normed algebra, with the sup norm.

Русский

Произведение конечного числа нормированных алгебр является нормированной алгеброй с суп-нормой.

LaTeX

$$$\\mathrm{NormedAlgebra}_{\\mathbb{K}}(\\prod_{i=1}^n E_i)$$$

Lean4

/-- The product of two normed algebras is a normed algebra, with the sup norm. -/
instance normedAlgebra {E F : Type*} [SeminormedRing E] [SeminormedRing F] [NormedAlgebra 𝕜 E] [NormedAlgebra 𝕜 F] :
    NormedAlgebra 𝕜 (E × F) :=
  { Prod.normedSpace, Prod.algebra 𝕜 E F with }

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