Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-29 18:18 c25bd03e

View on Github →

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

Estimated changes

Modified src/algebra/order/field.lean

added theorem div_self_le_one

Modified src/data/real/nnreal.lean

modified theorem nnreal.div_self_le