Commit 2021-03-04 08:43 76aee25d

View on Github →

refactor(big_operators/basic): move prod_mul_prod_compl (#6526) Several lemmas were unnecessarily in src/data/fintype/card.lean, and I've relocated them to src/algebra/big_operators/basic.lean.

Estimated changes

Modified src/algebra/big_operators/basic.lean

added theorem finset.prod_compl_mul_prod

added theorem finset.prod_mul_prod_compl

added theorem is_compl.prod_mul_prod

Modified src/data/fintype/basic.lean

added theorem finset.union_compl

Modified src/data/fintype/card.lean

deleted theorem finset.prod_compl_mul_prod

deleted theorem finset.prod_mul_prod_compl

deleted theorem is_compl.prod_mul_prod