Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-28 19:34 50ed0e4c

View on Github →

feat(algebra/big_operators): add congruence rule and morphism laws

Estimated changes

Modified algebra/big_operators.lean

added theorem finset.prod_congr

modified theorem finset.prod_empty

added theorem finset.prod_hom

modified theorem finset.prod_image

modified theorem finset.prod_insert

added theorem finset.prod_inv_distrib

modified theorem finset.prod_mul_distrib

modified theorem finset.prod_singleton

modified theorem finset.prod_to_finset_of_nodup

added theorem finset.sum_sub_distrib

Modified data/finset/fold.lean

added theorem finset.fold_congr

modified theorem finset.fold_hom

modified theorem finset.fold_image

modified theorem finset.fold_insert

modified theorem finset.fold_op_distrib

modified theorem finset.fold_singleton

added theorem list.map_congr