Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-09 05:24 6ccfe5a3

View on Github →

feat(algebra/ordered...): Two tiny lemmas (#1522)

feat(algebra/ordered...): Two tiny lemmas
style(src/algebra/ordered_field) Co-Authored-By: Reid Barton rwbarton@gmail.com

Estimated changes

Modified src/algebra/floor.lean

added theorem lt_of_nat_ceil_lt

modified theorem nat_ceil_lt_add_one

Modified src/algebra/ordered_field.lean

added theorem one_div_lt