English
The localized multiplication is associative with the localized scalar action: (x y) z = x (y z).
Русский
Локализованное умножение ассоциативно сочетается с локализованным скалярным действием: (x y) z = x (y z).
LaTeX
$$$ (x y) \; z = x \; (y \; z) $$$
Lean4
@[to_additive]
protected theorem mul_smul (x y : R[S⁻¹]) (z : X[S⁻¹]) : (x * y) • z = x • y • z := by
-- Porting note: `assoc_rw` was not ported yet
cases x with
| _ r₁ s₁
cases y with
| _ r₂ s₂
cases z with
| _ r₃ s₃
rcases oreDivMulChar' r₁ r₂ s₁ s₂ with ⟨ra, sa, ha, ha'⟩; rw [ha']; clear ha'
rcases oreDivSMulChar' r₂ r₃ s₂ s₃ with ⟨rb, sb, hb, hb'⟩; rw [hb']; clear hb'
rcases oreCondition ra sb with ⟨rc, sc, hc⟩
rw [oreDiv_smul_char (ra * r₂) r₃ (sa * s₁) s₃ (rc * rb) sc]; swap
· rw [← mul_assoc _ ra, hc, mul_assoc, hb, ← mul_assoc]
rw [← mul_assoc, mul_smul]
symm; apply oreDiv_smul_char
rw [Submonoid.coe_mul, Submonoid.coe_mul, ← mul_assoc, ← hc, mul_assoc _ ra, ← ha, mul_assoc]
