Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-24 10:50 1dda1cd6

View on Github →

feat(algebra/big_operators/finprod): a few more lemmas (#8843)

  • versions of monoid_hom.map_finprod that assume properties of f : M →* N instead of finiteness of the support;
  • finsum_smul, smul_finsum, finprod_inv_distrib: missing analogues of lemmas from finset.prod/finset.sum API.

Estimated changes

added theorem finprod_inv_distrib
added theorem finsum_smul
added theorem mul_equiv.map_finprod
added theorem smul_finsum