Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-08 18:05 22c8faed

View on Github →

feat(data/nat/pairing): ported data/nat/pairing.lean from Lean2

Estimated changes

added def nat.mkpair
added theorem nat.mkpair_unpair
added def nat.unpair
added theorem nat.unpair_lt
added theorem nat.unpair_lt_aux
added theorem nat.unpair_mkpair