charPoly — Mathlib

English

The family {char he hL w : W →ᵇ ℂ} with w ∈ W forms a star-subalgebra of the bounded complex-valued functions on V; namely, the range of charAlgHom.

Русский

Семейство функций, заданных как w ↦ (v ↦ e(L(v,w))), образует звездообразную подалгебру ограниченных функций V → ℂ; то есть это диапазон charAlgHom.

LaTeX

$$$\\text{charPoly}(he,hL) = \\operatorname{range}(\\text{charAlgHom}(he,hL)) \\\\ \\subseteq \\text{StarSubalgebra}(\\mathbb{C}, V \\to_b \\mathbb{C}).$$$

Lean4

/-- The star-subalgebra of polynomials. -/
noncomputable def charPoly (he : Continuous e) (hL : Continuous fun p : V × W ↦ L p.1 p.2) : StarSubalgebra ℂ (V →ᵇ ℂ)
    where
  toSubalgebra := (charAlgHom he hL).range
  star_mem' hx := star_mem_range_charAlgHom he hL hx

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