ofNat_sub_den

Mathlib.Data.Rat.Lemmas

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem ofNat_sub_den (n : ℕ) (q : ℚ) : (ofNat(n) - q).den = q.den :=
  natCast_sub_den ..

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

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

Разделы

Аффилиация

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