Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-13 06:04 e13fd486

View on Github →

docs(data/nat/pairing): add module docstring (#7897)

Estimated changes

Modified src/computability/partrec_code.lean

Modified src/computability/primrec.lean

Modified src/data/equiv/list.lean

Modified src/data/nat/pairing.lean

deleted theorem nat.le_mkpair_left

deleted theorem nat.le_mkpair_right

added theorem nat.left_le_mkpair

added theorem nat.right_le_mkpair

deleted theorem nat.unpair_le_left

deleted theorem nat.unpair_le_right

added theorem nat.unpair_left_le

added theorem nat.unpair_right_le