mk_add_mk — Mathlib

English

The sum of two mk elements with possibly different s is mk (s'·m + s·m') (s · s').

Русский

Сумма элементов mk m1 s1 и mk m2 s2 равна mk (s2·m1 + s1·m2) (s1·s2).

LaTeX

$$$\text{mk } m_1 s_1 + \text{mk } m_2 s_2 = \text{mk } (s_2.\text{val} \cdot m_1 + s_1.\text{val} \cdot m_2) (s_1 \cdot s_2)$$$

Lean4

theorem mk_add_mk {m1 m2 : M} {s1 s2 : ℕ+} : mk m1 s1 + mk m2 s2 = mk (s2.val • m1 + s1.val • m2) (s1 * s2) :=
  LocalizedModule.mk_add_mk

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