Mathlib v3 is deprecated. Go to Mathlib v4

Theorem canonically_ordered_comm_semiring.mul_pos

Modification history

2022-11-06 23:41
src/algebra/order/ring/basic.lean
refactor(*): supremum of several recent refactoring PRs (#17381) …
Modified canonically_ordered_comm_semiring.mul_posView on Github →
2021-09-18 16:39
src/algebra/ordered_ring.lean
chore(data/real/ennreal, measure_theory/): use `≠ ∞` and `≠ 0` in assumptions (#9219)
Modified canonically_ordered_comm_semiring.mul_posView on Github →
2021-07-14 18:22
src/algebra/ordered_ring.lean
refactor(algebra/ordered_ring): use `mul_le_mul'` for `canonically_ordered_comm_semiring` (#8284) …
Added canonically_ordered_comm_semiring.mul_posView on Github →