quasispectrum_subset — Mathlib

English

In a nonunital ring with suitable scalar structure, the quasi-spectrum of an idempotent element p is contained in {0,1}: quasispectrum 𝕜 p ⊆ {0,1}.

Русский

В неединичном кольце с подходящей скалярной структурой квази-спектр идемпотентного элемента p содержится в {0,1}.

LaTeX

$$$$ \\text{quasispectrum } 𝕜(p) \\subseteq \\{0,1\\}. $$$$

Lean4

theorem quasispectrum_subset {𝕜 A : Type*} [Field 𝕜] [NonUnitalRing A] [Module 𝕜 A] [IsScalarTower 𝕜 A A]
    [SMulCommClass 𝕜 A A] {p : A} (hp : IsIdempotentElem p) : quasispectrum 𝕜 p ⊆ {0, 1} :=
  quasispectrum_eq_spectrum_inr' 𝕜 𝕜 p ▸ (hp.inr _ |>.spectrum_subset _)

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