Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC