squashSeq_eq_self_of_terminated — Mathlib

English

If the generalized continued fraction g has terminated at position n, then squashGCF g n equals g itself.

Русский

Если обобщённое непрерывное дробление g прекратилось на позиции n, то squashGCF g n равно самому g.

LaTeX

$$squashGCF(g,n) = g (when g terminates at n).$$

Lean4

/-- If the sequence already terminated at position `n + 1`, nothing gets squashed. -/
theorem squashSeq_eq_self_of_terminated (terminatedAt_succ_n : s.TerminatedAt (n + 1)) : squashSeq s n = s :=
  by
  change s.get? (n + 1) = none at terminatedAt_succ_n
  cases s_nth_eq : s.get? n <;> simp only [*, squashSeq]

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