Mathlib v3 is deprecated. Go to Mathlib v4

Theorem mul_self_pos

Modification history

2022-01-04 07:46

src/algebra/order/ring.lean

feat(algebra/order/ring): turn `mul_self_pos` into an `iff` (#11216)

Modified mul_self_pos View on Github →

2018-09-13 12:28

algebra/ordered_ring.lean

feat(algebra/ordered_ring): mul_self_pos

Added mul_self_pos View on Github →