of_partNum_eq_one — Mathlib

English

If the nth partial numerator equals a in the context of GenContFract.of, then a = 1.

Русский

Если на позиции n частный числитель gp.a равен a, полученный из of v, то a = 1.

LaTeX

$$$\\\\forall {a : K} \\\\Bigl((GenContFract.of v).partNums.get? n = Some a) \\\\Rightarrow a = 1\\\\)$$$

Lean4

/-- Shows that the partial numerators `aᵢ` are equal to one. -/
theorem of_partNum_eq_one {a : K} (nth_partNum_eq : (of v).partNums.get? n = some a) : a = 1 :=
  by
  obtain ⟨gp, nth_s_eq, gp_a_eq_a_n⟩ : ∃ gp, (of v).s.get? n = some gp ∧ gp.a = a :=
    exists_s_a_of_partNum nth_partNum_eq
  have : gp.a = 1 := (of_partNum_eq_one_and_exists_int_partDen_eq nth_s_eq).left
  rwa [gp_a_eq_a_n] at this

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