Commit 2023-03-15 16:02 ce7e9d53
View on Github →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.