Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-15 19:41 5f04e76e

View on Github →

feat(nat/basic): add some basic nat inequality lemmas (#937)

  • feat(nat/basic): add some basic nat inequality lemmas, useful as specific cases of existing ring cases since uses less hypothesis
  • feat(nat/basic): add some basic nat inequality lemmas, with convention fixes
  • feat(nat/basic): add some basic nat inequality lemmas, with convention fixes

Estimated changes