Commit 2026-10-18 00:43 44f0a202
View on Github →feat(Algebra/BigOperators): add theorems about prod of rotate of list (#44953) This PR add a theorem to handle List.prod of List.rotate, when we are working in a CommMonoid, and another one for the case that member in the list is pairwise commute.