Theorems · Definition · functional analysis

resolventSet

(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 resolvent set of a : A is the Set R consisting of those r : R for which r•1 - a is a unit of the algebra A.

Defined in

Mathlib.Algebra.Algebra.Spectrum.Basic

Cited by

30 results in Mathlib

Foundations

Depth 16 from the axioms · uses no axioms

Assumes

CommSemiringRingAlgebra