mathlib
d49636ec - doc(topology/open_subgroup): add module docstring (#10111)

Commit

4 years ago

doc(topology/open_subgroup): add module docstring (#10111) Also add a lattice instance.

Author

PatrickMassot

Parents