mathlib
19a156ae - refactor(algebra/ordered_ring): use `mul_le_mul'` for `canonically_ordered_comm_semiring` (#8284)

Commit
4 years ago
refactor(algebra/ordered_ring): use `mul_le_mul'` for `canonically_ordered_comm_semiring` (#8284) * use `canonically_ordered_comm_semiring`, not `canonically_ordered_semiring` as a namespace; * add an instance `canonically_ordered_comm_semiring.to_covariant_mul_le`; * drop `canonically_ordered_semiring.mul_le_mul` etc in favor of `mul_le_mul'` etc. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Author
Parents
Loading