[Merged by Bors] - feat(algebra/triv_sq_zero_ext): lemmas about big operators

[eric-wieser]

Some more results following on from #18384.

For now this just has the list lemmas. The multiset and finset lemmas are hard to state cleanly.

---

My attempt at stating the omitted multiset and finset versions can be found in the git history of this PR as

lemma snd_multiset_prod {ι} [decidable_eq ι] [comm_semiring R] [add_comm_monoid M]
  [module R M] [module Rᵐᵒᵖ M] [is_central_scalar R M]
  (s : multiset ι) (f : ι → tsze R M) :
  (s.map f).prod.snd =
    (s.map (λ i, ((s.erase i).map (λ j, (f j).fst)).prod • (f i).snd)).sum :=

lemma snd_prod {ι} [decidable_eq ι] [comm_semiring R] [add_comm_monoid M]
  [module R M] [module Rᵐᵒᵖ M] [is_central_scalar R M]
  (s : finset ι) (f : ι → tsze R M) :
  (∏ i in s, f i).snd =
    ∑ i in s, (∏ j in s.erase i, (f j).fst) • (f i).snd :=

With some extra machinery it should be possible to avoid [decidable_eq ι].

[ocfnash]

Thanks!

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests