mathlib
43531676 - doc(topology/basic): add a few doc strings [skip ci] (#1775)

Commit

6 years ago

doc(topology/basic): add a few doc strings [skip ci] (#1775) * doc(topology/basic): add a few doc strings * Apply suggestions from code review

References

Author

urkud

Committer

mergify[bot]

Parents