mathlib
71b36b6f - chore(order/category): Partially revert categories (#18690)

Commit
2 years ago
chore(order/category): Partially revert categories (#18690) It was pointed out in leanprover-community/mathlib4#3164 that certain changes in #18657 were unsound. This PR reverts those unsound changes. Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Author
Parents
Loading