instNormedAlgebra — Mathlib

English

If 𝕜 is a normed field and γ a normed ring with an 𝕜-module structure, then C(α, γ) has a NormedAlgebra structure over 𝕜 when α is compact.

Русский

Пусть 𝕜 - нормированное поле и γ - нормированное кольцо с модулем над 𝕜; тогда C(α, γ) образует NormedAlgebra над 𝕜, если α компактно.

LaTeX

$$NormedAlgebra 𝕜 (C(α, γ))$$

Lean4

instance : NormedAlgebra 𝕜 C(α, γ) :=
  { ContinuousMap.normedSpace, ContinuousMap.algebra with }

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