exists_rat_eq_nth_conv — Mathlib

English

There exists q ∈ ℚ such that (of v).convs n = q.cast, i.e., the nth convergent corresponds to a rational.

Русский

Существует q ∈ ℚ такое, что (of v).convs n = q.cast, то есть n-й конвергент соответствует рациональному.

LaTeX

$$$\\exists q : \\mathbb{Q}, \\ (of\\, v).convs n = q.cast$$$

Lean4

/-- Every finite convergent corresponds to a rational number. -/
theorem exists_rat_eq_nth_conv : ∃ q : ℚ, (of v).convs n = (q : K) :=
  by
  rcases exists_rat_eq_nth_num v n with ⟨Aₙ, nth_num_eq⟩
  rcases exists_rat_eq_nth_den v n with ⟨Bₙ, nth_den_eq⟩
  use Aₙ / Bₙ
  simp [nth_num_eq, nth_den_eq, conv_eq_num_div_den]

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