[Merged by Bors] - feat: add lemma List.prod_map_ite_eq

[BoltonBailey]

Proves that the (product) sum of a list mapped through a function of the form if x = a then ... else ... is equal to the (product) sum over the list mapped through the else condition, (times) plus an additional factor about the number of times a appears.

Upstreamed from another project.

---

[urkud]

Is it from an open source project? If yes, then please link. Also, what do you think about adding these generic lemmas?

namespace List

variable {α M : Type*} [CommMonoid M]

@[to_additive]
lemma prod_map_ite (p : α → Prop) [DecidablePred p] (f g : α → β) (l : List α) :
    (l.map fun a ↦ if p a then f a else g a).prod =
      ((l.filter fun a ↦ p a).map f) * ((l.filter fun a ↦ ¬p a).map g) := _

@[to_additive]
lemma prod_map_filter_mul_prod_map_filter_not (p : α → Prop) [DecidablePred p] (f : α → M) (l : List α) :
    -- See `Finset.prod_filter_mul_prod_filter_not`

[BoltonBailey]

Seems good, I have added these.

[Ruben-VandeVelde]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

[github-actions]

PR summary 75218f0978

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ prod_map_filter_mul_prod_map_filter_not
+ prod_map_ite
+ prod_map_ite_eq

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[fpvandoorn]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style