exists_gcf_pair_rat_eq_nth_conts — Mathlib

English

For any v and n, there exists conts such that (of v).conts n = conts.map (Rat.cast).

Русский

Для любого v и n существует conts такой, что (of v).conts n = conts.map (Rat.cast).

LaTeX

$$$\\exists conts : Pair\\mathbb{Q},\\ (of\\, v).conts n = conts.map (Rat.cast)$$$

Lean4

theorem exists_gcf_pair_rat_eq_nth_conts : ∃ conts : Pair ℚ, (of v).conts n = (conts.map (↑) : Pair K) := by
  rw [nth_cont_eq_succ_nth_contAux]; exact exists_gcf_pair_rat_eq_of_nth_contsAux v <| n + 1

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