Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-24 01:02 8255507e

View on Github →

feat(data/pnat/basic): Add strong induction on pnat (#4736) I added strong induction on pnat. (This was from a previous PR that I am splitting.)

Estimated changes