Zulip Chat Archive

Stream: maths

Topic: subgroup module docstring.


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 11 2020 at 14:47):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 11 2020 at 14:50):

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

view this post on Zulip Patrick Massot (Sep 11 2020 at 14:50):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 11 2020 at 14:51):

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

view this post on Zulip 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...

view this post on Zulip Bryan Gin-ge Chen (Sep 11 2020 at 14:52):

Here it is: #4115

view this post on Zulip 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?

view this post on Zulip 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