Topic: perm vs sym
Johan Commelin (Sep 28 2018 at 12:06):
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 (Sep 28 2018 at 12:13):
Oh, the PR is from the
determinants branch on community mathlib.
Chris Hughes (Sep 28 2018 at 13:00):
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 (Sep 28 2018 at 14:04):
@Kenny Lau @Chris Hughes I removed
Last updated: May 12 2021 at 08:14 UTC