Theorem finRotate_succ_apply

Modification history

2026-10-10 09:42
Mathlib/Logic/Equiv/Fin/Rotate.lean
chore: delete deprecated declarations to March 2026 (#44240)
Deleted finRotate_succ_applyView on Github →
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_applyView on Github →
2025-03-12 17:40
Mathlib/Logic/Equiv/Fin/Basic.lean
feat(Logic/Equiv/Fin): add `finRotate` lemma (#22251)
Modified finRotate_succ_applyView on Github →
2023-01-23 18:47
Mathlib/Logic/Equiv/Fin.lean
feat: port Logic.Equiv.Fin (#1745)
Added finRotate_succ_applyView on Github →