squashGCF_nth_of_lt — Mathlib

English

For m < n, the m-th component of squashGCF g (n+1) equals the m-th component of g.

Русский

Для m < n, m-ая компонента squashGCF g (n+1) равна m-ой компоненте g.

LaTeX

$$$(\\text{squashGCF}(g,(n+1))).s.get? m = g.s.get? m \text{ for } m < n$.$$

Lean4

/-- The values before the squashed position stay the same. -/
theorem squashGCF_nth_of_lt {m : ℕ} (m_lt_n : m < n) : (squashGCF g (n + 1)).s.get? m = g.s.get? m := by
  simp only [squashGCF, squashSeq_nth_of_lt m_lt_n]

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