mathlib
eb05a940 - feat(order/filter/germ): define `filter.germ` (#3172)

Commit
5 years ago
feat(order/filter/germ): define `filter.germ` (#3172) Actually we already had this definition under the name `filter_product`.
Author
Parents
Loading