subring

Stream: maths

[Kevin Buzzard]

So for better or worse, we have subgroup and 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 subring.lean to 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 subring immediately.

Is there anyone who thinks this is a terrible idea, or knows of someone who has started on this already?

[Anne Baanen]

I saw that @Yury G. Kudryashov recently defined bundled subsemirings.

[Kevin Buzzard]

Yury, would it be a good first PR to make subrings on top of this?

[Yury G. Kudryashov]

I think yes. It's mostly about replacing add_submonoid by add_subgroup everywhere.