Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-13 12:28 46502df9

View on Github →

feat(algebra/ordered_ring): mul_self_pos

Estimated changes

modified theorem mul_le_one
added theorem mul_self_pos