Mathlib v3 is deprecated. Go to Mathlib v4

Theorem div_lt_self

Modification history

2022-01-11 13:55

src/algebra/order/field.lean

feat(algebra/order/field): lemmas relating `a / b` and `a` when `1 ≤ b` and `1 < b` (#11333) …

Added div_lt_self View on Github →