perm vs sym

Stream: maths

[Johan Commelin]

In the determinants PR https://github.com/leanprover/mathlib/pull/378#issuecomment-425396841 I have copy-pasted @Kenny Laus take on the symmetric group (group_theory/sym.lean). But in group_theory/perm.lean we already have a version by @Chris Hughes. Both files are several hundred lines long. There is substantial overlap, but both take their own approach in several places. I would like to use this thread to discuss how to merge these two files.

[Johan Commelin]

Oh, the PR is from the determinants branch on community mathlib.

[Chris Hughes]

I think I've done everything necessary for determinants, now that fintype is in mathlib, so anything that Kenny's done should probably be PRed separately from determinants.

[Johan Commelin]

@Kenny Lau @Chris Hughes I removed group_theory/sym.lean.