resolvent — Mathlib

English

The resolvent map r ↦ (algebraMap r − a)⁻¹ gives the resolvent in A, noncomputable in general.

Русский

Разрешённое отображение r ↦ (algebraMap r − a)⁻¹ даёт разрешение в A; в общем случае оно не вычислимо.

LaTeX

$$$\operatorname{resolvent}(a)(r) = (\mathrm{algebraMap}_{R}^{A} r - a)^{-1}$$$

Lean4

/-- 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`. -/
noncomputable def resolvent (a : A) (r : R) : A :=
  Ring.inverse (↑ₐ r - a)

Похожие утверждения