mathlib
fa4a805d - feat(order/category): Forgetful functor `NonemptyFinLinOrd ⥤ FinPartOrd` (#18948)

Commit

2 years ago

feat(order/category): Forgetful functor `NonemptyFinLinOrd ⥤ FinPartOrd` (#18948) Also fix a wrong docstring

Author

YaelDillies

Parents