Commit 2023-02-27 10:42 824f9ae9
View on Github →feat(algebra/order/ring/canonical): add canonically_ordered_comm_semiring.to_ordered_comm_monoid (#18504)
Also merge finset.prod_le_prod' with finset.prod_le_prod''.
Mathlib 4 version is leanprover-community/mathlib4#2510