## Stream: maths

### Topic: subring

#### Kevin Buzzard (Jul 20 2020 at 16:24):

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 (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 add_submonoid by add_subgroup everywhere.

Last updated: May 19 2021 at 02:10 UTC