Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_compl.prod_mul_prod

Modification history

2021-03-04 08:43
src/algebra/big_operators/basic.lean
refactor(big_operators/basic): move prod_mul_prod_compl (#6526) …
Modified is_compl.prod_mul_prodView on Github →
2020-11-02 20:27
src/data/fintype/card.lean
chore(data/fintype/card): add a few lemmas (#4877) …
Added is_compl.prod_mul_prodView on Github →