succ_nth_conv'_eq_squashGCF_nth_conv'

English

For a general field K, convs'(n+1) equals the nth convergents of the squashGCF at position n: g.convs'(n+1) = (squashGCF g n).convs' n.

Русский

Для поля K выполняется: convs'(n+1) = (squashGCF g n).convs' n.

LaTeX

$$$$g.convs'(n+1) = (\text{squashGCF}(g,n)).convs'(n).$$$$

Lean4

/-- `convs'` returns the same value for a gcf and the corresponding squashed gcf at the
squashed position. -/
theorem succ_nth_conv'_eq_squashGCF_nth_conv' : g.convs' (n + 1) = (squashGCF g n).convs' n := by
  cases n with
  | zero => cases g_s_head_eq : g.s.get? 0 <;> simp [g_s_head_eq, squashGCF, convs', convs'Aux, Stream'.Seq.head]
  | succ => simp only [succ_succ_nth_conv'Aux_eq_succ_nth_conv'Aux_squashSeq, convs', squashGCF]

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