convergent_of_int — Mathlib

English

If ξ is an integer, all its convergents equal ξ.

Русский

Если ξ целое число, все конвергенты равны ξ.

LaTeX

$$$$\\forall \\xi\\in\\mathbb{Z},\\; \\xi.convergent n = \\xi.$$$$

Lean4

/-- If `ξ` is an integer, all its convergents equal `ξ`. -/
@[simp]
theorem convergent_of_int {ξ : ℤ} (n : ℕ) : convergent ξ n = ξ :=
  by
  cases n
  · simp only [convergent_zero, floor_intCast]
  · simp only [convergent_succ, floor_intCast, fract_intCast, convergent_of_zero, add_zero, inv_zero]

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