Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-27 09:36 6a79f8a1

View on Github →

feat(data/int/basic): to_nat lemmas (#1479)

  • feat(data/int/basic): of_nat lemmas
  • Adding lt_of_to_nat_lt
  • reversing sides of <->

Estimated changes

added theorem int.lt_of_to_nat_lt
added theorem int.lt_to_nat
modified theorem int.to_nat_le
added theorem int.to_nat_lt_to_nat