mkRat_add_mkRat_of_den

Mathlib.Data.Rat.Lemmas

URI: https://scilib.ai/kg/mathlib#Rat.mkRat_add_mkRat_of_den

← MathLib Explorer

English

For any integers n1, n2 and nonzero d, mkRat n1 d + mkRat n2 d = mkRat (n1 + n2) d.

Русский

Для любых целых n1, n2 и не нуля d верно: mkRat n1 d + mkRat n2 d = mkRat (n1+n2) d.

LaTeX

$$mkRat(n1, d) + mkRat(n2, d) = mkRat(n1 + n2, d)$$

Lean4

theorem mkRat_add_mkRat_of_den (n₁ n₂ : Int) {d : Nat} (h : d ≠ 0) : mkRat n₁ d + mkRat n₂ d = mkRat (n₁ + n₂) d := by
  rw [mkRat_add_mkRat _ _ h h, ← add_mul, mkRat_mul_right h]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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