mem_quasispectrum_iff — Mathlib

English

For semifield R, ring A, and algebra structure, an element x lies in quasispectrum(R,a) precisely when x equals 0 or x lies in spectrum(R,a).

Русский

Для semifield R, кольца A и структуры алгебры элемент x принадлежит quasispectrum(R,a) тогда и только тогда, когда x = 0 или x принадлежит spectrum(R,a).

LaTeX

$$$x \in \operatorname{quasispectrum}(R,a) \iff x = 0 \lor x \in \operatorname{spectrum}(R,a)$$$

Lean4

theorem mem_quasispectrum_iff {R A : Type*} [Semifield R] [Ring A] [Algebra R A] {a : A} {x : R} :
    x ∈ quasispectrum R a ↔ x = 0 ∨ x ∈ spectrum R a := by simp [quasispectrum_eq_spectrum_union_zero]

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