Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-25 19:48 82e78ce8

View on Github →

feat(algebra/big_operators/finprod): add lemma finprod_mem_finset_of_product (#7439)

Estimated changes

Modified src/algebra/big_operators/finprod.lean

added theorem finprod_curry

added theorem finprod_curry₃

added theorem finprod_mem_finset_product'

added theorem finprod_mem_finset_product

added theorem finprod_mem_finset_product₃

added theorem finprod_mem_mul_support

added theorem finset.mul_support_of_fiberwise_prod_subset_image

Modified src/data/support.lean

added theorem function.mul_support_along_fiber_finite_of_finite

added theorem function.mul_support_along_fiber_subset