mk_cancel_common_left — Mathlib

English

For any s, s' ∈ S and m ∈ M, mk(s' • m) (s' • s) = mk(m) s, showing a left-cancellation property of common factors.

Русский

Для любых s, s' ∈ S и m ∈ M выполняется mk(s' • m) (s' • s) = mk(m) s, что демонстрирует левую отмену общих множителей.

LaTeX

$$$\\mathrm{mk}(s'\\cdot m, s'\\cdot s) = \\mathrm{mk}(m, s)$$$

Lean4

@[simp]
theorem mk_cancel_common_left (s' s : S) (m : M) : mk (s' • m) (s' * s) = mk m s :=
  mk_eq.mpr
    ⟨1, by
      simp only [mul_smul, one_smul]
      rw [smul_comm]⟩

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