smul'_mk — Mathlib

English

The statement mk'_smul_mk asserts the compatibility of scalar mk' action with the localized mk, i.e., IsLocalization.mk' T r s • mk m s' = mk (r • m) (s · s').

Русский

Утверждение mk'_smul_mk устанавливает совместимость скалярного действия mk' с локализованным mk: 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 smul'_mk (r : R) (s : S) (m : M) : r • mk m s = mk (r • m) s := by simpa only [one_mul] using mk_smul_mk r m 1 s

Похожие утверждения