Mathlib v3 is deprecated. Go to Mathlib v4

Theorem lt_mul_self

Modification history

2022-08-05 22:34

src/algebra/order/ring.lean

feat(algebra/order/ring): lt_mul_{left,right,self} (#15848)

Added lt_mul_self View on Github →