English
The action of IsLocalization.mk' on an element m by r distributes over the localized multiplication: IsLocalization.mk' T r s • mk m s' = mk (r • m) (s · s').
Русский
Действие mk' на элемент m домножает локализованный элемент так, что IsLocalization.mk' T r s • mk m s' = mk (r • m) (s · s').
LaTeX
$$$\\mathrm{IsLocalization.mk'}(T, r, s) \\; \\cdot \\; \\mathrm{mk}(m,s') = \\mathrm{mk}(r \\cdot m, s \\cdot s')$$$
Lean4
theorem mk'_smul_mk (r : R) (m : M) (s s' : S) : IsLocalization.mk' T r s • mk m s' = mk (r • m) (s * s') :=
by
rw [smul_def, mk_eq]
obtain ⟨c, hc⟩ := IsLocalization.eq.mp <| IsLocalization.mk'_sec T (IsLocalization.mk' T r s)
use c
simp_rw [← mul_smul, Submonoid.smul_def, Submonoid.coe_mul, ← mul_smul, ← mul_assoc, mul_comm _ (s' : R), mul_assoc,
hc]
