toNormedAlgebra — Mathlib

English

A StarSubalgebra S of A induces a NormedAlgebra structure on S via the inclusion map.

Русский

Подстановка StarSubalgebra S внутри A порождает структуру NormedAlgebra на S через инклюзию.

LaTeX

$$$ \text{NormedAlgebra}_{\,\mathbb{K}}(S) = \text{InducedNormedAlgebra}_{\mathbb{K}}(S, A, S. subtype) $$$

Lean4

instance toNormedAlgebra {𝕜 A : Type*} [NormedField 𝕜] [StarRing 𝕜] [SeminormedRing A] [StarRing A] [NormedAlgebra 𝕜 A]
    [StarModule 𝕜 A] (S : StarSubalgebra 𝕜 A) : NormedAlgebra 𝕜 S :=
  NormedAlgebra.induced 𝕜 S A S.subtype

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