Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-21 00:48 4abf9618

View on Github →

feat(algebra/big_operators): product over coerced fintype (#7236)

Estimated changes

Modified src/algebra/big_operators/basic.lean

added theorem finset.prod_finset_coe

added theorem finset.prod_subtype

added theorem fintype.prod_finset_coe

Modified src/data/fintype/card.lean

deleted theorem finset.prod_subtype