mk_cancel

Mathlib.Algebra.Module.LocalizedModule.Basic

URI: https://scilib.ai/kg/mathlib#LocalizedModule.mk_cancel

English

For any s, s' ∈ S and m ∈ M, mk(s' • m) (s * s') = mk(m) s, a right-cancellation analogue to the previous lemma.

Русский

Для любых 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 (s : S) (m : M) : mk (s • m) s = mk m 1 :=
  mk_eq.mpr ⟨1, by simp⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru