mathlib
634dfc8a - feat(order/*): Missing order lifting instances (#12154)

Commit

3 years ago

feat(order/*): Missing order lifting instances (#12154) Add a few missing pullbacks of order instances.

Author

YaelDillies

Parents