Kevin Buzzard (Jul 20 2020 at 16:24):
So for better or worse, we have
is_subgroup, and the same for monoids. One advantage of doing things the way we did them (didn't remove
is_X but added
X anyway) was that
is_X became available immediately. Another advantage is that in both cases I got an Imperial student to write
is_X and in both cases I believe the student learnt a lot. I am proposing doing the same with subrings now. We don't have
subring, we do have
is_subring, so I'm proposing making a new file
subring.lean, moving the current
is_subring.lean and getting a student to bundle subrings so they can have access to bundled subrings for another project.
The refactoring is happening. Scott and I (mostly Scott so far) are working on removing
is_subgroup from a bunch of files, in WIP PR #3321 . The advantage of the procedure I'm outlining above is that students of mine can access
Is there anyone who thinks this is a terrible idea, or knows of someone who has started on this already?
Anne Baanen (Jul 20 2020 at 20:57):
I saw that @Yury G. Kudryashov recently defined bundled subsemirings.
Kevin Buzzard (Jul 20 2020 at 22:33):
Yury, would it be a good first PR to make subrings on top of this?
Yury G. Kudryashov (Jul 22 2020 at 05:57):
I think yes. It's mostly about replacing
Last updated: May 19 2021 at 02:10 UTC