add_intCast_den — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem add_intCast_den (q : ℚ) (n : ℤ) : (q + n).den = q.den :=
  by
  apply Nat.dvd_antisymm
  · simpa using add_den_dvd q n
  · simpa using add_den_dvd (q + n) (-n)

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