getLast_replicate_succ — Mathlib

English

For any m and a, the last element of replicate(m+1, a) equals a.

Русский

Для любых m и a, последний элемент replicate(m+1, a) равен a.

LaTeX

$$$\forall m\, a, (\mathrm{replicate}(m+1,a)).getLast\, (\mathrm{ne\_nil\_of\_length\_eq\_add\_one}\, \mathrm{length\_replicate}) = a$$$

Lean4

theorem getLast_replicate_succ (m : ℕ) (a : α) :
    (replicate (m + 1) a).getLast (ne_nil_of_length_eq_add_one length_replicate) = a :=
  by
  simp only [replicate_succ']
  exact getLast_append_singleton _

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