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
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):
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