mk_add_mk_left

Mathlib.GroupTheory.DivisibleHull

URI: https://scilib.ai/kg/mathlib#DivisibleHull.mk_add_mk_left

English

The left addition distributes: mk m1 s + mk m2 s = mk (m1 + m2) s.

Русский

Левое сложение распределено: mk m1 s + mk m2 s = mk (m1 + m2) s.

LaTeX

$$$\text{mk } m_1 s + \text{mk } m_2 s = \text{mk } (m_1 + m_2) s$$$

Lean4

theorem mk_add_mk_left {m1 m2 : M} {s : ℕ+} : mk m1 s + mk m2 s = mk (m1 + m2) s :=
  by
  rw [mk_add_mk, mk_eq_mk]
  exact ⟨1, by simp [smul_smul]⟩

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

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

Разделы

Аффилиация

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