Mathlib v3 is deprecated. Go to Mathlib v4

Theorem div_self_le_one

Modification history

2021-12-29 18:18

src/algebra/order/field.lean

feat(algebra/order/field): prove `a / a ≤ 1` (#11118)

Added div_self_le_one View on Github →