English
Let x in R, m in M, s and t in S. The multiplication in the localized module identifies the localization of A with the action of x on m, i.e. the element obtained by first forming mk' A x s and then mk' f m t equals mk' f (x · m) (s · t).
Русский
Пусть x ∈ R, m ∈ M, s, t ∈ S. Умножение в локализованном модуле соответствует локализации: mk' A x s · mk' f m t = mk' f (x · m) (s · t).
LaTeX
$$$$ [x,s] \\cdot [m,t] = [x\\cdot m, s\\cdot t] $$$$
Lean4
theorem mk'_smul_mk' (x : R) (m : M) (s t : S) : IsLocalization.mk' A x s • mk' f m t = mk' f (x • m) (s * t) :=
by
apply smul_injective f (s * t)
conv_lhs => simp only [smul_assoc, mul_smul, smul_comm t]
simp only [mk'_cancel', map_smul, Submonoid.smul_def s]
rw [← smul_assoc, IsLocalization.smul_mk'_self, algebraMap_smul]
