mathlib3
6486e9b3 - chore(order/rel_classes): Removed unnecessary `classical` (#11180)

Commit

4 years ago

chore(order/rel_classes): Removed unnecessary `classical` (#11180) Not sure what that was doing here.

Author

vihdzp

Parents