Theorems · Definition · functional analysis

quasispectrum

(R : Type u_1) → {A : Type u_2} → [inst : CommSemiring R] → [inst_1 : NonUnitalRing A] → [Module R A] → A → Set R

If A is a non-unital R-algebra, the R-quasispectrum of a : A consists of those r : R such that if r is invertible (in R), then -(r⁻¹ • a) is not quasiregular. The quasispectrum is precisely the spectrum in the unitization when R is a commutative ring. See Unitization.quasispectrum_eq_spectrum_inr.

Defined in

Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Cited by

292 results in Mathlib

Foundations

Depth 19 from the axioms, rests on 240 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringNonUnitalRingModule