English
For α, m, n and xs, ys, we have: Function.comp (Fin.append xs ys) Fin.rev equals Function.comp (Fin.append (Function.comp ys Fin.rev) (Function.comp xs Fin.rev)) (Fin.cast …).
Русский
Для девятки: Function.comp (Fin.append xs ys) Fin.rev равен Function.comp (Fin.append (Function.comp ys Fin.rev) (Function.comp xs Fin.rev)) (Fin.cast …).
LaTeX
$$$\\mathrm{Function.comp}(\\mathrm{Fin.append}\\ xs\\ ys)\\ \\mathrm{Fin.rev} = \\mathrm{Function.comp}(\\mathrm{Fin.append}(\\mathrm{Function.comp}\\ ys\\ \\mathrm{Fin.rev},\\ \\mathrm{Function.comp}\\ xs\\ \\mathrm{Fin.rev}))\\ (\\mathrm{Fin.cast}\\ ⋯).$$$
Lean4
/-- Repeat `a` `m` times. For example `Fin.repeat 2 ![0, 3, 7] = ![0, 3, 7, 0, 3, 7]`. -/
def «repeat» (m : ℕ) (a : Fin n → α) : Fin (m * n) → α
| i => a i.modNat
