English
For rings A and B and a ∈ A, b ∈ B, the quasispectrum of the pair (a,b) in A×B equals the union of the quasispectra of a and of b.
Русский
Для колец A и B и элементов a ∈ A, b ∈ B, квазиспектр пары (a,b) в произведении A×B равен объединению квазиспектров a и b.
LaTeX
$$$$ \operatorname{quasispectrum}(R, (a,b)) = \operatorname{quasispectrum}(R,a) \cup \operatorname{quasispectrum}(R,b) $$$$
Lean4
theorem quasispectrum_eq [CommSemiring R] [NonUnitalRing A] [NonUnitalRing B] [Module R A] [Module R B] (a : A)
(b : B) : quasispectrum R (⟨a, b⟩ : A × B) = quasispectrum R a ∪ quasispectrum R b :=
by
apply compl_injective
ext r
simp only [quasispectrum, Set.mem_compl_iff, Set.mem_setOf_eq, not_forall, not_not, Set.mem_union]
by_cases hr : IsUnit r
· lift r to Rˣ using hr with r' hr'
simp [isQuasiregular_prod_iff]
· simp [hr]
