Commit 2023-11-03 16:55 edcf9202

View on Github →

feat: expand Finset.noncommProd API (#8155)

Estimated changes

Modified Mathlib/Data/Finset/NoncommProd.lean

added theorem Finset.mul_noncommProd_erase

added theorem Finset.noncommProd_erase_mul

added theorem Finset.noncommProd_induction

added theorem Multiset.mul_noncommProd_erase

added theorem Multiset.noncommProd_erase_mul

added theorem Multiset.noncommProd_induction

Modified Mathlib/Data/List/BigOperators/Basic.lean

modified theorem List.prod_erase

added theorem List.prod_erase_of_comm

added theorem List.prod_induction

Modified Mathlib/Data/Multiset/Basic.lean

added theorem Multiset.erase_cons_tail_of_mem

added theorem Multiset.map_erase_of_mem