quasispectrum_eq_spectrum_union_zero

English

In the semifield setting, the quasispectrum of a equals the spectrum of a together with the element 0: quasispectrum(R,a) = spectrum(R,a) ∪ {0}.

Русский

В условиях semifield квази-спектр элемента a совпадает со спектром элемента a вместе с нулём: quasispectrum(R,a) = spectrum(R,a) ∪ {0}.

LaTeX

$$$\operatorname{quasispectrum}(R,a) = \operatorname{spectrum}(R,a) \cup \{0\}$$$

Lean4

theorem quasispectrum_eq_spectrum_union_zero (R : Type*) {A : Type*} [Semifield R] [Ring A] [Algebra R A] (a : A) :
    quasispectrum R a = spectrum R a ∪ {0} :=
  by
  convert quasispectrum_eq_spectrum_union R a
  simp

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