intCast_sub_den

Mathlib.Data.Rat.Lemmas

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

English

Let n be an integer and q a rational number. Then the denominator of (n − q) equals the denominator of q.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem intCast_sub_den (n : ℤ) (q : ℚ) : (n - q).den = q.den := by rw [sub_eq_add_neg, intCast_add_den, neg_den]

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

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

Разделы

Аффилиация

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