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.