mk'_add_mk' — Mathlib

English

The sum of two fractions mk' f m1 s1 and mk' f m2 s2 has a concrete expression as a single mk' with a linear combination of m1 and m2 and the product s1 s2.

Русский

Сумма дробей mk' f m1 s1 и mk' f m2 s2 записывается как одна дробь mk' f (s2·m1 + s1·m2) (s1·s2).

LaTeX

$$$mk' f m_1 s_1 + mk' f m_2 s_2 = mk' f (s_2\\cdot m_1 + s_1\\cdot m_2) (s_1\\cdot s_2)$$$

Lean4

theorem mk'_add_mk' (m₁ m₂ : M) (s₁ s₂ : S) : mk' f m₁ s₁ + mk' f m₂ s₂ = mk' f (s₂ • m₁ + s₁ • m₂) (s₁ * s₂) :=
  by
  delta mk'
  rw [← map_add, LocalizedModule.mk_add_mk]

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