Commit 2021-09-13 13:59 ad625833
View on Github →chore(algebra/big_operators): add a lemma (#9120)
(product over s.filter p) * (product over `s.filter (λ x, ¬p x)) = product over s
chore(algebra/big_operators): add a lemma (#9120)
(product over s.filter p) * (product over `s.filter (λ x, ¬p x)) = product over s