mathlib
e6eeade6 - chore(order/{rel_iso, directed}): monotone functions and rel_homs are directed
Commit
5 years ago
Author
Parents