Fin.prod

Stream: mathlib4

[Antoine Chambert-Loir]

Mathlib has docs#Fin.prod that is a nice way to have products on non necessarily commutative monoids, but most functions about products indexed by a map from Fin are written in the Finset.prod style and assume commutativity. Example: docs#Fin.prod_snoc.
On the other hand, docs#Set.mem_pow is written using docs#List.ofFn and lacks API.
Would it make sense to generalize all the results in #Mathlib.Algebra.BigOperators.Fin by writing them in docs#Fin.prod-style?

[Ruben Van de Velde]

No, I don't think so

[Ruben Van de Velde]

There's docs#List.prod for ordered products

[Antoine Chambert-Loir]

So docs#Fin.prod should be deprecated then?

[Antoine Chambert-Loir]

And in any case, the results in Mathlib.Algebra.BigOperators.Fin.lean would hold without commutativity assumption if written for lists.

[Eric Wieser]

I think Fin.prod exists because batteries needed products and didn't want to absorb Finset