add_mk — Mathlib

English

Adding two fractions in the localization by the same denominator yields the sum with the common denominator.

Русский

Сложение двух дробей в локализации с одинаковым знаменателем даёт сумму с этим знаменателем.

LaTeX

$$$$ \\mathrm{mk} a b + \\mathrm{mk} c b = \\mathrm{mk}(a + c) b $$$$

Lean4

theorem add_mk (a b c d) : (mk a b : Localization M) + mk c d = mk ((b : R) * c + (d : R) * a) (b * d) :=
  by
  rw [add_comm (b * c) (d * a), mul_comm b d]
  exact OreLocalization.oreDiv_add_oreDiv

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