Commit 2023-01-21 14:22 ddae32a2

View on Github →

feat: port Data.Fintype.BigOperators (#1742)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Fintype/BigOperators.lean

added theorem Equiv.prod_comp'

added theorem Equiv.prod_comp

added theorem Fin.prod_univ_eq_prod_range

added theorem Finset.card_pi

added theorem Finset.prod_attach_univ

added theorem Finset.prod_fiberwise

added theorem Finset.prod_fin_eq_prod_range

added theorem Finset.prod_toFinset_eq_subtype

added theorem Finset.prod_univ_pi

added theorem Finset.prod_univ_sum

added theorem Fintype.card_eq_sum_ones

added theorem Fintype.card_fun

added theorem Fintype.card_pi

added theorem Fintype.card_piFinset

added theorem Fintype.eq_of_subsingleton_of_prod_eq

added theorem Fintype.prod_bool

added theorem Fintype.prod_congr

added theorem Fintype.prod_eq_mul

added theorem Fintype.prod_eq_one

added theorem Fintype.prod_eq_single

added theorem Fintype.prod_extend_by_one

added theorem Fintype.prod_fiberwise

added theorem Fintype.prod_option

added theorem Fintype.prod_sum_elim

added theorem Fintype.prod_sum_type

added theorem Fintype.sum_pow_mul_eq_add_pow

added theorem Function.Bijective.prod_comp

added theorem card_vector