Commit 2026-01-29 07:34 b9b99d35

feat: add API lemmas for Multiset.prod_map and finprod (#34533) We add lemmas Multiset.prod_map_prod, finprod_le_finprod and finprod_le_finprod' that fill holes in the API. Note: the naming of the latter two parallels Finset.prod_le_prod and Finset.prod_le_prod' (which are actually used in the proofs). The import increase should be OK as it is not a public import (it is needed for the proofs). This is used in [#34330](https://github.com/leanprover-community/mathlib4/pull/34330).