Mathlib v3 is deprecated. Go to Mathlib v4

Theorem zero_le_mul

Modification history

2019-09-14 05:00
src/algebra/ordered_ring.lean
chore(data/*): flipping inequalities (#1436) …
Deleted zero_le_mulView on Github →
2017-12-19 04:59
algebra/ordered_ring.lean
feat(data/ordinal): sup, cofinality, subtraction
Modified zero_le_mulView on Github →
2017-08-29 19:20
topology/ennreal.lean
feat(topology/ennreal): add extended non-negative real numbers
Added zero_le_mulView on Github →