quasispectrum_inr_eq — Mathlib

English

Equality between quasispectrum and spectrum under the inr injection holds for unitization.

Русский

Существование равенства между квази-спектром и спектром через инр-вставку в Unitization.

LaTeX

$$quasispectrum(R, a) = spectrum(R, (Unitization.inr a))$$

Lean4

theorem quasispectrum_inr_eq (R S : Type*) {A : Type*} [Semifield R] [Field S] [NonUnitalRing A] [Algebra R S]
    [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [Module R A] [IsScalarTower R S A] (a : A) :
    quasispectrum R (a : Unitization S A) = quasispectrum R a :=
  by
  rw [quasispectrum_eq_spectrum_union_zero, quasispectrum_eq_spectrum_inr' R S]
  simpa using zero_mem_spectrum_inr _ _ _

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