English
For a: Fin n → α and k ∈ Fin(mn), repeating m across the reversed index equals repeating on the composed function a after reversing indices, i.e., Fin.repeat m a k.rev = Fin.repeat m (a ∘ Fin.rev) k.
Русский
Для a: Fin n → α и k ∈ Fin(mn), повторение по м вдоль развернутого индекса равно повторению по функции a после разворота индексов: Fin.repeat m a k.rev = Fin.repeat m (a ∘ Fin.rev) k.
LaTeX
$$$\\mathrm{Fin.repeat}(m)\\,a\\ (k.\\mathrm{rev}) = \\mathrm{Fin.repeat}(m)\\,(a \\circ \\mathrm{Fin.rev})\\ k$$$
Lean4
theorem repeat_rev (a : Fin n → α) (k : Fin (m * n)) : Fin.repeat m a k.rev = Fin.repeat m (a ∘ Fin.rev) k :=
congr_arg a k.modNat_rev
