Theorems · Theorem · functional analysis

Prod.quasispectrum_eq

∀ {A : Type u_2} {B : Type u_3} {R : Type u_4} [inst : CommSemiring R] [inst_1 : NonUnitalRing A]
  [inst_2 : NonUnitalRing B] [inst_3 : Module R A] [inst_4 : Module R B] (a : A) (b : B),
  quasispectrum R (a, b) = quasispectrum R a ∪ quasispectrum R b

Defined in

Mathlib.Algebra.Algebra.Spectrum.Pi

Cited by

1 results in Mathlib

Foundations

Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringNonUnitalRingNonUnitalRingModuleModule