add_ofNat_den

Mathlib.Data.Rat.Lemmas

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

English

Let q be a rational number and n a natural number. Then (q + ofNat(n)).den = q.den.

Русский

Пусть q — рациональное число, n — натуральное. Тогда (q + ofNat(n)).den = q.den.

LaTeX

$$$\operatorname{den}(q + \operatorname{ofNat}(n)) = \operatorname{den}(q)$$$

Lean4

@[simp]
theorem add_ofNat_den (q : ℚ) (n : ℕ) : (q + ofNat(n)).den = q.den :=
  add_natCast_den q n

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

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

Разделы

Аффилиация

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