spectrum_subset — Mathlib

English

If p is idempotent (p^2 = p) in a 𝕜-algebra A, then its spectrum is contained in {0,1}: σ(p) ⊆ {0,1}.

Русский

Если p идемпотентен (p^2 = p) в алгебре над 𝕜, то его спектр лежит в {0,1}: σ(p) ⊆ {0,1}.

LaTeX

$$$$ \\sigma(\\,p\,) \\subseteq \\{0,1\\}. $$$$

Lean4

theorem spectrum_subset (𝕜 : Type*) {A : Type*} [Field 𝕜] [Ring A] [Algebra 𝕜 A] {p : A} (hp : IsIdempotentElem p) :
    spectrum 𝕜 p ⊆ {0, 1} := by
  nontriviality A
  apply Set.image_subset_iff.mp (spectrum.subset_polynomial_aeval p (X ^ 2 - X)) |>.trans
  refine fun a ha => eq_zero_or_one_of_sq_eq_self ?_
  simpa [pow_two p, hp.eq, sub_eq_zero] using ha

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