mathlib

ca17a181 - feat(algebra/pointwise): introduce `canonically_ordered_comm_semiring` on `set_semiring` ... (#11580)

feat(algebra/pointwise): introduce `canonically_ordered_comm_semiring` on `set_semiring` ... (#11580) ... assuming multiplication is commutative (there is no `canonically_ordered_`~~comm~~`_semiring` structure). Also prove the relevant `no_zero_divisors` and `covariant_class` properties of addition and multiplication. Co-authored-by: Damiano Testa <maskal@CLD-E854D68C.ads.warwick.ac.uk> Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>