Zulip Chat Archive
Stream: mathlib4
Topic: Product of a tuple of elements of a group
Yury G. Kudryashov (Jan 10 2026 at 07:42):
What's the Mathlib way to write the product of f k, k : Fin n, if the multiplication is noncommutative? In my case, f k are ContinuousLinearMaps. I see at least these options:
- docs#Fin.prod from Batteries, with virtually no API
(List.finRange n).map f |>.prodwhich seems too specific
Did I miss something? Should I add API about Fin.prod, or should I use something else?
Yury G. Kudryashov (Jan 10 2026 at 08:02):
For more context: I need a formula for fderiv K (f^[n]) x, where x is not a fixed point of f.
Aaron Liu (Jan 10 2026 at 08:07):
in CGT we needed to evaluate a polynomial on ordinals which have noncommutative addition and multiplication
Aaron Liu (Jan 10 2026 at 08:08):
Aaron Liu (Jan 10 2026 at 08:08):
looks like it's just List.sum
Eric Wieser (Jan 10 2026 at 08:41):
(List.ofFn f).prod?
Eric Wieser (Jan 10 2026 at 08:43):
What did I do for docs#fderiv_pow' ? nevermind, I guess that was a sum
Violeta Hernández (Jan 11 2026 at 13:37):
Aaron Liu said:
Great reminder that I need to upstream this to Mathlib as Ordinal.CNF.eval.
Last updated: Feb 28 2026 at 14:05 UTC