Commit 2025-01-29 05:19 40e01655

View on Github →

chore(Perm/Fin): generalize from Fin n.succ to Fin n (#21193) ... adding [NeZero n] as needed. Cherry-picked from #21112

Estimated changes

modified theorem Fin.coe_cycleRange_of_le
modified theorem Fin.coe_cycleRange_of_lt
modified theorem Fin.cycleRange_apply
added theorem Fin.cycleRange_mk_zero
modified theorem Fin.cycleRange_of_eq
modified theorem Fin.cycleRange_of_gt
modified theorem Fin.cycleRange_of_le
modified theorem Fin.cycleRange_of_lt
modified theorem Fin.cycleRange_self
modified theorem Fin.cycleRange_symm_zero
deleted theorem Fin.cycleRange_zero'
modified theorem Fin.cycleRange_zero
modified theorem Fin.cycleType_cycleRange
modified theorem Fin.isCycle_cycleRange