Commit 2023-01-19 11:36 12aa913c

View on Github →

feat: port Algebra.BigOperators.Ring (#1645)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/BigOperators/Ring.lean

added theorem Finset.dvd_sum

added theorem Finset.mul_sum

added theorem Finset.prod_add

added theorem Finset.prod_add_ordered

added theorem Finset.prod_nat_cast

added theorem Finset.prod_one_sub_ordered

added theorem Finset.prod_pow_eq_pow_sum

added theorem Finset.prod_powerset

added theorem Finset.prod_powerset_insert

added theorem Finset.prod_range_cast_nat_sub

added theorem Finset.prod_sub_ordered

added theorem Finset.prod_sum

added theorem Finset.sum_boole_mul

added theorem Finset.sum_div

added theorem Finset.sum_mul

added theorem Finset.sum_mul_boole

added theorem Finset.sum_mul_sum

added theorem Finset.sum_pow_mul_eq_add_pow

added theorem Finset.sum_range_succ_mul_sum_range_succ