English
Let α be a family indexed by Fin(n+1). For any a: Fin n → α, Fin.repeat 1 a equals a composed with Fin.cast (Nat.one_mul _), i.e., the single repetition just reindexes a without changing its values.
Русский
Пусть α — семейство объектов, индексируемых Fin(n+1). Для любой a: Fin n → α, Fin.repeat 1 a равен a ∘ Fin.cast (Nat.one_mul _), то есть повторение один раз просто переразмещает индексы без изменения значений.
LaTeX
$$$\\mathrm{Fin.repeat}(1)\\,a = a \\circ \\mathrm{Fin.cast}(\\mathrm{Nat.one\\_mul}\\,\\_)$$$
Lean4
@[simp]
theorem repeat_one (a : Fin n → α) : Fin.repeat 1 a = a ∘ Fin.cast (Nat.one_mul _) :=
by
generalize_proofs h
apply funext
rw [(Fin.rightInverse_cast h.symm).surjective.forall]
intro i
simp [modNat, Nat.mod_eq_of_lt i.is_lt]
