mathlib

824f9ae9 - feat(algebra/order/ring/canonical): add `canonically_ordered_comm_semiring.to_ordered_comm_monoid` (#18504)

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