English
The rotation map is identified with the inverse decomposition: finRotate(n+1) = decomposeFin.symm(1, finRotate(n)).
Русский
Поворотная карта совпадает с обратным разложением: finRotate(n+1) = decomposeFin.symm(1, finRotate(n)).
LaTeX
$$$ \\mathrm{finRotate}(n+1) = \\mathrm{decomposeFin.symm}(1, \\mathrm{finRotate}(n))$$$
Lean4
theorem finRotate_succ_eq_decomposeFin {n : ℕ} : finRotate n.succ = decomposeFin.symm (1, finRotate n) :=
by
ext i
cases n; · simp
refine Fin.cases ?_ (fun i => ?_) i
· simp
rw [coe_finRotate, decomposeFin_symm_apply_succ, if_congr i.succ_eq_last_succ rfl rfl]
split_ifs with h
· simp [h]
·
rw [Fin.val_succ, Function.Injective.map_swap Fin.val_injective, Fin.val_succ, coe_finRotate, if_neg h,
Fin.val_zero, Fin.val_one, swap_apply_of_ne_of_ne (Nat.succ_ne_zero _) (Nat.succ_succ_ne_one _)]
