Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-01 20:04 5694d152

View on Github →

feat(data/nat/basic): nat.le_rec_on (#585)

Estimated changes

Modified src/data/nat/basic.lean

added def nat.le_rec_on

added theorem nat.le_rec_on_injective

added theorem nat.le_rec_on_self

added theorem nat.le_rec_on_succ'

added theorem nat.le_rec_on_succ

added theorem nat.le_rec_on_surjective

added theorem nat.le_rec_on_trans

added theorem nat.of_le_succ