Theorem finRotate_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) …
Added finRotate_symm_applyView on Github →