spectrum_eq — Mathlib

English

For a pair (a,b) in A × B, spectrum_R(a,b) equals spectrum_R(a) ∪ spectrum_R(b).

Русский

Для пары (a,b) ∈ A × B спектр равен объединению спектров: spectrum_R(a,b) = spectrum_R(a) ∪ spectrum_R(b).

LaTeX

$$$\operatorname{spectrum}_R(\langle a,b \rangle) = \operatorname{spectrum}_R(a) \cup \operatorname{spectrum}_R(b)$$$

Lean4

theorem spectrum_eq [CommSemiring R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (a : A) (b : B) :
    spectrum R (⟨a, b⟩ : A × B) = spectrum R a ∪ spectrum R b :=
  by
  apply compl_injective
  simp_rw [spectrum, Set.compl_union, compl_compl, resolventSet, ← Set.setOf_and, Prod.isUnit_iff, algebraMap_apply,
    mk_sub_mk]

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