Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-27 20:58 b031441f

View on Github →

feat(algebra): add small theory of big operators on commutative monoids

Estimated changes

Created algebra/big_operators.lean

added theorem finset.prod_empty

added theorem finset.prod_image

added theorem finset.prod_insert

added theorem finset.prod_mul_distrib

added theorem finset.prod_singleton

added theorem finset.prod_to_finset

added theorem finset.prod_union

added theorem finset.prod_union_inter_eq

added theorem foldl_mul_assoc

added theorem foldl_mul_eq_mul_foldr

added theorem prod_append

added theorem prod_cons

added theorem prod_eq_of_perm

added theorem prod_join

added theorem prod_nil

added theorem prod_replicate