Mathlib v3 is deprecated. Go to Mathlib v4

Theorem zero_le_mul_right

Modification history

2020-05-18 13:38
src/algebra/ordered_ring.lean
refactor(algebra): merge init_.algebra into algebra (#2707) …
Modified zero_le_mul_rightView on Github →
2020-04-01 01:14
src/algebra/ordered_ring.lean
feat(data/nat/basic): `simp` lemmas about inequalities with `bit*` (#2207) …
Added zero_le_mul_rightView on Github →