Theorems · Definition · functional analysis

spectrum

(R : Type u) → {A : Type v} → [inst : CommSemiring R] → [inst_1 : Ring A] → [Algebra R A] → A → Set R

Given a commutative ring R and an R-algebra A, the spectrum of a : A is the Set R consisting of those r : R for which r•1 - a is not a unit of the algebra A. The spectrum is simply the complement of the resolvent set.

Defined in

Mathlib.Algebra.Algebra.Spectrum.Basic

Cited by

510 results in Mathlib

Foundations

Depth 17 from the axioms, rests on 187 definitions · uses no axioms

Assumes

CommSemiringRingAlgebra