mathlib

c5ea4cdd - feat(group_theory/perm): define the permutation `(0 1 ... (i : fin n))` (#6815)

feat(group_theory/perm): define the permutation `(0 1 ... (i : fin n))` (#6815) 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. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Yakov Pechersky <ffxen158@gmail.com>