Theorem List.prod_rotate_of_pairwise_commute

Modification history

2026-10-18 00:43
Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean
feat(Algebra/BigOperators): add theorems about prod of rotate of list (#44953) …
Added List.prod_rotate_of_pairwise_commuteView on Github →