Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-06 14:05 93a64dae

View on Github →

chore(data/pnat/basic): add mk_le_mk, mk_lt_mk, coe_le_coe, coe_lt_coe (#2613)

Estimated changes

Modified src/data/pnat/basic.lean

added theorem pnat.coe_le_coe

added theorem pnat.coe_lt_coe

added theorem pnat.mk_le_mk

added theorem pnat.mk_lt_mk

Modified src/data/pnat/intervals.lean

modified theorem pnat.Ico.mem