Theorems · Definition · functional analysis

resolvent

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

Given an a : A where A is an R-algebra, the resolvent is a map R → A which sends r : R to (algebraMap R A r - a)⁻¹ when r ∈ resolvent R A and 0 when r ∈ spectrum R A.

Defined in

Mathlib.Algebra.Algebra.Spectrum.Basic

Cited by

23 results in Mathlib

Foundations

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

Assumes

CommSemiringRingAlgebra