Theorem Fin.pos_of_ne_zero

Modification history

2025-08-18 09:17

Mathlib/Data/Fin/Basic.lean

feat(GroupTheory/Perm/Fin): add Fin.cycleIcc and refactor cycleRange (#27014) …

Modified Fin.pos_of_ne_zero View on Github →

2023-12-31 21:44

Mathlib/Data/Fin/Basic.lean

feat: Fin CharP and lemmas for Fin rollover (#9033)

Added Fin.pos_of_ne_zero View on Github →