Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-22 16:32 f004d327

View on Github →

feat(data/nat): various lemmas (#1017)

  • feat(data/nat): various lemmas
  • protect a definition
  • fixes
  • Rob's suggestions
  • Mario’s proof (Working offline, let’s see what Travis says)
  • minigolf

Estimated changes

added theorem nat.div_eq_self
added theorem nat.div_le_div_left
added theorem nat.eq_of_dvd_quot_one
added theorem nat.eq_zero_of_le_div
added theorem nat.eq_zero_of_le_half
added theorem nat.eq_zero_of_mul_le
added theorem nat.lt_mul_of_div_lt