commutativity and BigOperators

Stream: mathlib4

[Ralf Stephan]

What is the reason why BigOperators require commutativity? Naively, as long as the factors are in the right order, it doesn't seem necessary.
https://github.com/leanprover-community/mathlib4/blob/8aa21118d3b9ea49ff7b6c77155e03df0f057bbb/Mathlib/Algebra/BigOperators/Group/Finset.lean#L23

[Yakov Pechersky]

The factors are in the right order is only stateable for a List. A Finset, rather, is the quotient over all possible orders of the elements, since it's a subtype of a Multiset

[Yakov Pechersky]

We do have docs#Finset.noncommProd

[Yakov Pechersky]

Where commutativity is required only on the elements of the finset itself, not the whole type

[Ralf Stephan]

Thanks. Is there an easy way to restate a statement that uses $\prod$ in terms of a List?

[Bolton Bailey]

The canonical way would probably be to use docs#List.map and docs#List.sum. It would be nice to have the notation, but no one has written this yet.