natCast_add_den

Mathlib.Data.Rat.Lemmas

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

English

Let q be a rational number and n a natural number. Then the denominator of (n + q) equals the denominator of q.

Русский

Пусть q — рациональное число, n — натуральное. Знаменатель (n + q) равен знаменателю q.

LaTeX

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

Lean4

@[simp]
theorem natCast_add_den (n : ℕ) (q : ℚ) : (n + q).den = q.den :=
  mod_cast intCast_add_den n q

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

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

Разделы

Аффилиация

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