mem_spectrum_inr_of_not_isUnit — Mathlib

English

If r ∈ R is not a unit, then r belongs to the spectrum of a inside the unitization: r ∈ spectrum(R, a as Unitization R A).

Русский

Если r ∈ R не является обратимым элементом, то он принадлежит спектру a в единичной декомпозиции: r ∈ spectrum(R, a в Unitization R A).

LaTeX

$$r ∈ R, ¬IsUnit r ⇒ r ∈ spectrum(R, (a : Unitization R A))$$

Lean4

theorem mem_spectrum_inr_of_not_isUnit {R A : Type*} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A]
    [SMulCommClass R A A] (a : A) (r : R) (hr : ¬IsUnit r) : r ∈ spectrum R (a : Unitization R A) := fun h ↦
  hr <| by simpa [map_sub] using h.map (fstHom R A)

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