mathlib3
1732f9cf - chore(topology): golf (#16585)

Commit
3 years ago
chore(topology): golf (#16585) 2 minor golfs from an old branch
Author
Parents
Loading