English
Addition on the Ore localization is associative: (x + y) + z = x + (y + z).
Русский
Сложение на локализации Оре ассоциативно: (x + y) + z = x + (y + z).
LaTeX
$$$(x + y) + z = x + (y + z)$$
Lean4
protected theorem add_assoc (x y z : X[S⁻¹]) : x + y + z = x + (y + z) :=
by
induction x with
| _ r₁ s₁
induction y with
| _ r₂ s₂
induction z with
| _ r₃ s₃
rcases oreDivAddChar' r₁ r₂ s₁ s₂ with ⟨ra, sa, ha, ha'⟩; rw [ha']; clear ha'
rcases oreDivAddChar' (sa • r₁ + ra • r₂) r₃ (sa * s₁) s₃ with ⟨rc, sc, hc, q⟩; rw [q]; clear q
simp only [smul_add, add_assoc]
simp_rw [← add_oreDiv, ← OreLocalization.expand']
congr 2
· rw [OreLocalization.expand r₂ s₂ ra (ha.symm ▸ (sa * s₁).2)]; congr; ext; exact ha
· rw [OreLocalization.expand r₃ s₃ rc (hc.symm ▸ (sc * (sa * s₁)).2)]; congr; ext; exact hc
