## Stream: maths

### Topic: subgroup module docstring.

#### Patrick Massot (Sep 11 2020 at 14:35):

https://leanprover-community.github.io/mathlib_docs/group_theory/subgroup.html starts with a lot of misleading links because the module docstring doesn't use full names. For instance closure and subtype link to the wrong thing.

#### Kevin Buzzard (Sep 11 2020 at 14:47):

Nice catch! What is the fix? You really want to write subgroup.closure in the docstring?

#### Kevin Buzzard (Sep 11 2020 at 14:49):

Oh, comap doesn't even link to anything, presumably because there is no comap in the root namespace.

#### Kevin Buzzard (Sep 11 2020 at 14:50):

Probably the same will be true for submonoids, subsemirings and subrings.

#### Patrick Massot (Sep 11 2020 at 14:50):

I'm afraid the only fix is to write subgroup.closure in the docstring.

#### Bryan Gin-ge Chen (Sep 11 2020 at 14:51):

I'm making a PR at the moment that fully qualifies the names.

#### Kevin Buzzard (Sep 11 2020 at 14:51):

Thanks! I'll get back to making these video lectures which need to be done within about three weeks...

#### Bryan Gin-ge Chen (Sep 11 2020 at 14:52):

Here it is: #4115

#### Patrick Massot (Sep 11 2020 at 15:01):

Speaking of subgroups, does anyone knows whether we proved that the image by a morphism of the closure of some set is the closure of the image?

#### Yury G. Kudryashov (Sep 15 2020 at 06:39):

Let's try src#monoid_hom.map_closure

Last updated: May 12 2021 at 08:14 UTC