mem_resolventSet_of_left_right_inverse

English

Let a be an element of an R-algebra A. If there exist b,c ∈ A such that (algebraMap(R,A)(r) − a)·b = 1 and c·(algebraMap(R,A)(r) − a) = 1, then r belongs to the resolvent set of a over R.

Русский

Пусть a ∈ A, где A является модулем над R и R-алгеброй А. Если существуют b,c ∈ A такие, что (algebraMap(R,A)(r) − a)·b = 1 и c·(algebraMap(R,A)(r) − a) = 1, то r принадлежит резольвентному множеству a над R.

LaTeX

$$$\bigl(\exists b,c \in A\;:\; (\operatorname{algebraMap}(R,A)(r) - a)\,b = 1 \land c\, (\operatorname{algebraMap}(R,A)(r) - a) = 1\bigr) \Rightarrow r \in \operatorname{resolventSet}(R,a)$$$

Lean4

theorem mem_resolventSet_of_left_right_inverse {r : R} {a b c : A} (h₁ : (↑ₐ r - a) * b = 1) (h₂ : c * (↑ₐ r - a) = 1) :
    r ∈ resolventSet R a :=
  Units.isUnit ⟨↑ₐ r - a, b, h₁, by rwa [← left_inv_eq_right_inv h₂ h₁]⟩

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