exists_int_eq_of_partDen — Mathlib

English

If the nth partial denominator is b, then there exists an integer z with b = z in K.

Русский

Если на позиции n частной знаменателя стоит b, то существует целое z такое, что b = z в K.

LaTeX

$$$\\\\forall {b : K} \\\\Bigl((GenContFract.of v).partDens.get? n = Some b) \\\\Rightarrow \\\\Exists z : \\\\mathbb{Z}, b = (z : K)\\\\)$$$

Lean4

/-- Shows that the partial denominators `bᵢ` correspond to an integer. -/
theorem exists_int_eq_of_partDen {b : K} (nth_partDen_eq : (of v).partDens.get? n = some b) : ∃ z : ℤ, b = (z : K) :=
  by
  obtain ⟨gp, nth_s_eq, gp_b_eq_b_n⟩ : ∃ gp, (of v).s.get? n = some gp ∧ gp.b = b :=
    exists_s_b_of_partDen nth_partDen_eq
  have : ∃ z : ℤ, gp.b = (z : K) := (of_partNum_eq_one_and_exists_int_partDen_eq nth_s_eq).right
  rwa [gp_b_eq_b_n] at this

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