exists_rat_eq_nth_num — Mathlib

English

There exists a rational q with (of v).nums n = q, i.e., the nth numerator comes from a rational.

Русский

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

LaTeX

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

Lean4

theorem exists_rat_eq_nth_num : ∃ q : ℚ, (of v).nums n = (q : K) :=
  by
  rcases exists_gcf_pair_rat_eq_nth_conts v n with ⟨⟨a, _⟩, nth_cont_eq⟩
  use a
  simp [num_eq_conts_a, nth_cont_eq]

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