Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-10 15:28 5305d39a

View on Github →

feat(data/pnat/basic): succ as an order isomorphism between and ℕ+ (#15183) Couldn't find this in the library. Asked on Zulip in case anyone knew of this already.

Estimated changes