English
For r : Units R and a,b ∈ A, the inclusion ↑r ∈ σ(a·b) ⇔ ↑r ∈ σ(b·a) holds.
Русский
Для единицы r и элементов a,b ∈ A выполняется: ↑r ∈ σ(a·b) ⇔ ↑r ∈ σ(b·a).
LaTeX
$$$\uparrow r \in \sigma(a \cdot b) \iff \uparrow r \in \sigma(b \cdot a)$$$
Lean4
theorem unit_mem_mul_comm {a b : A} {r : Rˣ} : ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a) :=
by
have h₁ : ∀ x y : A, IsUnit (1 - x * y) → IsUnit (1 - y * x) :=
by
refine fun x y h => ⟨⟨1 - y * x, 1 + y * h.unit.inv * x, ?_, ?_⟩, rfl⟩
·
calc
(1 - y * x) * (1 + y * (IsUnit.unit h).inv * x) = 1 - y * x + y * ((1 - x * y) * h.unit.inv) * x := by
noncomm_ring
_ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.mul_val_inv, mul_one, sub_add_cancel]
·
calc
(1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) = 1 - y * x + y * (h.unit.inv * (1 - x * y)) * x := by
noncomm_ring
_ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.val_inv_mul, mul_one, sub_add_cancel]
have := Iff.intro (h₁ (r⁻¹ • a) b) (h₁ b (r⁻¹ • a))
rw [mul_smul_comm r⁻¹ b a] at this
simpa only [mem_iff, not_iff_not, Algebra.algebraMap_eq_smul_one, ← Units.smul_def, IsUnit.smul_sub_iff_sub_inv_smul,
smul_mul_assoc]
