apply_mem_spectrum — Mathlib

English

For every φ in the character space and every a ∈ A, the scalar φ(a) lies in the spectrum of a, i.e., φ(a) ∈ Spec(a).

Русский

Для каждого φ в пространстве характеров и каждого a ∈ A скаляр φ(a) принадлежит спектру элемента a, то есть φ(a) ∈ Spec(a).

LaTeX

$$$\forall \phi \in \mathrm{characterSpace}_{\mathbb{k}}(A),\; \forall a \in A:\ \phi(a) \in \operatorname{Spec}_{\mathbb{k}}(a).$$$

Lean4

theorem apply_mem_spectrum [Nontrivial 𝕜] (φ : characterSpace 𝕜 A) (a : A) : φ a ∈ spectrum 𝕜 a :=
  AlgHom.apply_mem_spectrum φ a

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