mathlib
a913b9b4 - chore(order/filter): move `filter.prod` and `filter.coprod` to a new file (#15937)

Commit

3 years ago

chore(order/filter): move `filter.prod` and `filter.coprod` to a new file (#15937) These lemmas and definitions are moved without changes.

Author

urkud

Parents