Commit 2024-09-18 11:42 d25f655d

View on Github →

feat: add smul_prod lemmas (#8807) From #6718.

Estimated changes

added theorem Finset.prod_smul
added theorem Finset.smul_prod'
modified theorem Finset.smul_prod
added theorem List.smul_prod'
modified theorem List.smul_prod
added theorem Multiset.smul_prod'
modified theorem Multiset.smul_prod
added theorem smul_finprod'
deleted theorem smul_finprod