mk_smul_mk — Mathlib

English

For any r ∈ R and s, s' ∈ S, the action mk' r s • mk m s' equals mk (r • m) (s · s').

Русский

Для любого r ∈ R и s, s' ∈ S выполняется mk' 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 t : S) : Localization.mk r s • mk m t = mk (r • m) (s * t) :=
  by
  rw [Localization.mk_eq_mk']
  exact mk'_smul_mk ..

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