squashGCF_eq_self_of_terminated — Mathlib

English

If the generalized continued fraction terminates at some position n, squashGCF g n equals g.

Русский

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

LaTeX

$$squashGCF(g,n) = g (when TerminatedAt g n).$$

Lean4

/-- If the gcf already terminated at position `n`, nothing gets squashed. -/
theorem squashGCF_eq_self_of_terminated (terminatedAt_n : TerminatedAt g n) : squashGCF g n = g := by
  cases n with
  | zero =>
    change g.s.get? 0 = none at terminatedAt_n
    simp only [squashGCF, terminatedAt_n]
  | succ =>
    cases g
    simp only [squashGCF, mk.injEq, true_and]
    exact squashSeq_eq_self_of_terminated terminatedAt_n

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