toNormedAlgebra — Mathlib

English

An instance equips the Subalgebra with a NormedAlgebra structure via the induced norm.

Русский

Подалгебра на коническом нормировании получает структуру NormedAlgebra через индуцированную норму.

LaTeX

$$$\\text{ToNormedAlgebra}(S)$$$

Lean4

instance toNormedAlgebra {𝕜 A : Type*} [SeminormedRing A] [NormedField 𝕜] [NormedAlgebra 𝕜 A] (S : Subalgebra 𝕜 A) :
    NormedAlgebra 𝕜 S :=
  NormedAlgebra.induced 𝕜 S A S.val

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