resolvent_eq — Mathlib

English

For any a ∈ A and r ∈ R, if r ∈ resolventSet(R,a), then resolvent(a,r) equals the inverse of (algebraMap(R,A)(r) − a) in A.

Русский

Пусть a ∈ A и r ∈ R. Если r принадлежит резольвентному множеству a, то резольвента resolvent(a,r) равна обратному элементу к (algebraMap(R,A)(r) − a) в A.

LaTeX

$$$\text{If } r \in \operatorname{resolventSet}(R,a)\text{, then } \operatorname{resolvent}(a,r) = (\operatorname{algebraMap}(R,A)(r) - a)^{-1}$$$

Lean4

theorem resolvent_eq {a : A} {r : R} (h : r ∈ resolventSet R a) : resolvent a r = ↑h.unit⁻¹ :=
  Ring.inverse_unit h.unit

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