isUnit_resolvent — Mathlib

English

For any r ∈ R and a ∈ A, r ∈ resolventSet(R,a) if and only if resolvent(a,r) is a unit in A.

Русский

Для любых r ∈ R и a ∈ A верно: r ∈ резольвентное множество(a) тогда и только тогда, когда резольвента resolvent(a,r) является единицей в A.

LaTeX

$$$r \in \operatorname{resolventSet}(R,a) \iff \operatorname{IsUnit}(\operatorname{resolvent}(a,r))$$$

Lean4

/-- The resolvent is a unit when the argument is in the resolvent set. -/
theorem isUnit_resolvent {r : R} {a : A} : r ∈ resolventSet R a ↔ IsUnit (resolvent a r) :=
  isUnit_ringInverse.symm

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