mathlib
88b8a77d - chore(topology/basic): backport a generalization to Sort (#18544)

Commit

2 years ago

chore(topology/basic): backport a generalization to Sort (#18544) mathport currently complains that these don't align.

Author

eric-wieser

Parents