algebraOfNormedAlgebra — Mathlib

English

If each B_i is a normed algebra over 𝕜, then the product space (i → B_i) carries a natural 𝕜-algebra structure, i.e., the algebra operations are defined pointwise.

Русский

Если каждый B_i является нормированным алгеброй над 𝕜, то произведение пространств i → B_i естественным образом образует 𝕜-алгебру с покоординатными операциями.

LaTeX

$$$\text{Algebra}_{\,\,\mathbb{K}}(\prod_i B_i)\;\text{with pointwise operations.}$$$

Lean4

/-- A variant of `Pi.algebra` that lean can't find otherwise. -/
instance _root_.Pi.algebraOfNormedAlgebra : Algebra 𝕜 (∀ i, B i) :=
  @Pi.algebra I 𝕜 B _ _ fun _ => NormedAlgebra.toAlgebra

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