English
Let α be a family of objects indexed by Fin(n+1). For any sequence a: Fin n → α, repeating zero times yields a canonical reindexing of a that discards the new last coordinate; i.e. Fin.repeat 0 a equals Fin.elim0 ∘ Fin.cast (Nat.zero_mul _).
Русский
Пусть α задаётся семейством объектов, индексируемых Fin(n+1). Для любой последовательности a: Fin n → α повторение нулём даёт каноническое переиндексирование a, и новое последнее слагаемое отброшено: Fin.repeat 0 a = Fin.elim0 ∘ Fin.cast (Nat.zero_mul _).
LaTeX
$$$\\operatorname{Fin.repeat}(0)\\,a = \\operatorname{Fin.elim0} \\circ \\operatorname{Fin.cast}(\\operatorname{Nat.zero\\_mul}\\,\\_).$$$
Lean4
@[simp]
theorem repeat_zero (a : Fin n → α) : Fin.repeat 0 a = Fin.elim0 ∘ Fin.cast (Nat.zero_mul _) :=
funext fun x => (x.cast (Nat.zero_mul _)).elim0
