mem_resolventSet_iff — Mathlib

English

Let r ∈ R and a ∈ A. Then r lies in the resolvent set of a over R if and only if algebraMap(R,A)(r) − a is a unit in A.

Русский

Пусть r ∈ R и a ∈ A. Тогда r ∈ резольвентное множество a над R тогда и только тогда, когда algebraMap(R,A)(r) − a является обратимым в A.

LaTeX

$$$r \in \operatorname{resolventSet}(R,a) \iff \operatorname{IsUnit}\bigl(\operatorname{algebraMap}(R,A)(r) - a\bigr)$$$

Lean4

theorem mem_resolventSet_iff {r : R} {a : A} : r ∈ resolventSet R a ↔ IsUnit (↑ₐ r - a) :=
  Iff.rfl

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