Theorem finRotate_succ_symm_apply

Modification history

2026-03-31 03:17

Mathlib/Logic/Equiv/Fin/Rotate.lean

chore(Logic/Equiv/Fin/Rotate): generalize from `Fin (n + 1)` to `Fin n` (#37338) …

Modified finRotate_succ_symm_apply View on Github →

2025-03-12 17:40

Mathlib/Logic/Equiv/Fin/Rotate.lean

feat(Logic/Equiv/Fin): add `finRotate` lemma (#22251)

Added finRotate_succ_symm_apply View on Github →