mathlib3

ce7e9d53 - feat(algebra/triv_sq_zero_ext): lemmas about big operators (#18488)

feat(algebra/triv_sq_zero_ext): lemmas about big operators (#18488) 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.