mathlib3
3592f45e - chore(order/filter/filter_product): fix `const_lt`, make `const_lt_iff` `@[simp, norm_cast]` (#17442)

Commit
2 years ago
chore(order/filter/filter_product): fix `const_lt`, make `const_lt_iff` `@[simp, norm_cast]` (#17442)
Author
Parents
Loading