Commit 2026-03-31 03:17 4ec5d95a

View on Github →

chore(Logic/Equiv/Fin/Rotate): generalize from Fin (n + 1) to Fin n (#37338) We can infer NeZero n if we already have i : Fin n.

Estimated changes

Modified Mathlib/Geometry/Polygon/Basic.lean

Modified Mathlib/Logic/Equiv/Fin/Rotate.lean

added theorem finRotate_apply

modified theorem finRotate_succ_apply

modified theorem finRotate_succ_symm_apply

added theorem finRotate_symm_apply