exists_rat_eq_nth_den — Mathlib

English

There exists a rational q with (of v).dens n = q.cast, i.e., the nth denominator is rational.

Русский

Существует рациональное число q такое, что (of v).dens n = q.cast.

LaTeX

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

Lean4

theorem exists_rat_eq_nth_den : ∃ q : ℚ, (of v).dens n = (q : K) :=
  by
  rcases exists_gcf_pair_rat_eq_nth_conts v n with ⟨⟨_, b⟩, nth_cont_eq⟩
  use b
  simp [den_eq_conts_b, nth_cont_eq]

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