mathlib3
ad625833 - chore(algebra/big_operators): add a lemma (#9120)

Commit

4 years ago

chore(algebra/big_operators): add a lemma (#9120) (product over `s.filter p`) * (product over `s.filter (λ x, ¬p x)) = product over s

Author

urkud

Parents