Theorem finRotate_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) …

Added finRotate_apply View on Github →