mk_add_mk — Mathlib

English

The addition of two canonical elements matches the canonical element formed by the linear combination with coefficients from S.

Русский

Складывание двух канонических элементов соответствует каноническому элементу, получаемому линейной комбинацией с коэффициентами из S.

LaTeX

$$$mk(m1,s1) + mk(m2,s2) = mk(s2 \\cdot m1 + s1 \\cdot m2, s1 s2).$$$

Lean4

theorem mk_add_mk {m1 m2 : M} {s1 s2 : S} : mk m1 s1 + mk m2 s2 = mk (s2 • m1 + s1 • m2) (s1 * s2) :=
  mk_eq.mpr <| ⟨1, rfl⟩

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