Commit 2021-08-10 10:54 5890afb1

feat(data/list/perm): perm.permutations (#8587) This proves the theorem from Zulip:

theorem perm.permutations {s t : list α} (h : s ~ t) : permutations s ~ permutations t := ...

It also introduces a permutations' function which has simpler equations (and indeed, this function is used to prove the theorem, because it is relatively easier to prove perm.permutations' first).