English
The scalar action is linear: (y + z) • x = y • x + z • x.
Русский
Скалярное действие линейно: (y + z) • x = y • x + z • x.
LaTeX
$$(y + z) \cdot x = y \cdot x + z \cdot x$$
Lean4
protected theorem add_smul (y z : R[S⁻¹]) (x : X[S⁻¹]) : (y + z) • x = y • x + z • x :=
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, q⟩
rw [q]
clear q
rw [OreLocalization.expand' r₂ s₂ sa]
rcases oreDivSMulChar' (sa • r₂) r₁ (sa * s₂) s₁ with ⟨rb, sb, hb, q⟩
rw [q]
clear q
have hs₃rasb : sb * ra * s₃ ∈ S := by
rw [mul_assoc, ← ha]
norm_cast
apply SetLike.coe_mem
rw [OreLocalization.expand _ _ _ hs₃rasb]
have ha' : ↑((sb * sa) * s₂) = sb * ra * s₃ := by simp [ha, mul_assoc]
rw [← Subtype.coe_eq_of_eq_mk ha']
rcases oreDivSMulChar' ((sb * ra) • r₃) r₁ (sb * sa * s₂) s₁ with ⟨rc, sc, hc, hc'⟩
rw [hc']
rw [oreDiv_add_char _ _ 1 sc (by simp [mul_assoc])]
rw [OreLocalization.expand' (sa • r₂ + ra • r₃) (sa * s₂) (sc * sb)]
simp only [smul_eq_mul, one_smul, Submonoid.smul_def, mul_add, Submonoid.coe_mul] at hb hc ⊢
rw [mul_assoc, hb, mul_assoc, ← mul_assoc _ ra, hc, ← mul_assoc, ← add_mul]
rw [OreLocalization.smul_cancel']
simp only [add_smul, ← mul_assoc, smul_smul]
