subgroup module docstring.

Stream: maths

[Patrick Massot]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Patrick Massot]

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

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

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

[Bryan Gin-ge Chen]

Here it is: #4115

[Patrick Massot]

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]

Let's try src#monoid_hom.map_closure