subgroups of a monoid

Stream: mathlib4

[Kevin Buzzard]

Why does Subgroup eat a group rather than a monoid? This came up in FLT-related work, because some Imperial students want to talk about maximal subfields of a K-algebra D where D is not a field (or even a division ring). They can't use docs#IntermediateField because this wants to eat fields. I realised that this convention stretches right down to the basics.

[Yury G. Kudryashov]

Workaround: you can use Subgroup (Units M)

[Yury G. Kudryashov]

If you want ⁻¹ on the subgroup to be defeq to the restriction of ⁻¹ on the original group (in case of groups), then you have to assume Group G.

[Kevin Buzzard]

This workaround does not work for intermediate fields (as subfields of a noncommutative ring) as there is no "maximal commutative subring" of a non-commutative ring.