Theorems · Theorem · functional analysis

Pi.quasispectrum_eq

∀ {ι : Type u_1} {R : Type u_4} {κ : ι → Type u_5} [Nonempty ι] [inst : CommSemiring R]
  [inst_1 : (i : ι) → NonUnitalRing (κ i)] [inst_2 : (i : ι) → Module R (κ i)] (a : (i : ι) → κ i),
  quasispectrum R a = ⋃ i, quasispectrum R (a i)

Defined in

Mathlib.Algebra.Algebra.Spectrum.Pi

Cited by

1 results in Mathlib

Foundations

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

Assumes

NonemptyCommSemiringNonUnitalRingModule