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.
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.