Equivalences involving ℕ
#
This file defines some additional constructive equivalences using Encodable
and the pairing
function on ℕ
.
@[simp]
@[simp]
@[simp]
An equivalence between ℤ
and ℕ
, through ℤ ≃ ℕ ⊕ ℕ
and ℕ ⊕ ℕ ≃ ℕ
.
ℕ
#This file defines some additional constructive equivalences using Encodable
and the pairing
function on ℕ
.
An equivalence between ℤ
and ℕ
, through ℤ ≃ ℕ ⊕ ℕ
and ℕ ⊕ ℕ ≃ ℕ
.