Zulip Chat Archive

Stream: maths

Topic: perm vs sym


view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 28 2018 at 12:13):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 28 2018 at 14:04):

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


Last updated: May 12 2021 at 08:14 UTC