mathlib

8c89ff7a - feat(group_theory/perm): define the permutation `(0 1 ... (i : fin n))`

feat(group_theory/perm): define the permutation `(0 1 ... (i : fin n))` I tried a number of definitions and it looks like this is the least awkward one to prove with. In any case, using the API should allow you to avoid unfolding the definition.