English
If r ∈ Rˣ and a ∈ Aˣ, and r ∈ resolventSet(R,a), then r⁻¹ ∈ resolventSet(R,a⁻¹).
Русский
Пусть r ∈ Rˣ и a ∈ Aˣ. Если r ∈ резольвентное множество( R, a ), то r⁻¹ ∈ резольвентное множество( R, a⁻¹ ).
LaTeX
$$$\text{If } r \in R^{\times} \text{ and } a \in A^{\times}, \; r \in \operatorname{resolventSet}(R,a) \Rightarrow r^{-1} \in \operatorname{resolventSet}(R, a^{-1})$$$
Lean4
theorem inv_mem_resolventSet {r : Rˣ} {a : Aˣ} (h : (r : R) ∈ resolventSet R (a : A)) :
(↑r⁻¹ : R) ∈ resolventSet R (↑a⁻¹ : A) :=
by
rw [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one, ← Units.smul_def] at h ⊢
rw [IsUnit.smul_sub_iff_sub_inv_smul, inv_inv, IsUnit.sub_iff]
have h₁ : (a : A) * (r • (↑a⁻¹ : A) - 1) = r • (1 : A) - a := by rw [mul_sub, mul_smul_comm, a.mul_inv, mul_one]
have h₂ : (r • (↑a⁻¹ : A) - 1) * a = r • (1 : A) - a := by rw [sub_mul, smul_mul_assoc, a.inv_mul, one_mul]
have hcomm : Commute (a : A) (r • (↑a⁻¹ : A) - 1) := by rwa [← h₂] at h₁
exact (hcomm.isUnit_mul_iff.mp (h₁.symm ▸ h)).2
