Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-26 15:58 d8fc0817

View on Github →

chore(data/pnat/basic): rename bot_eq_zero to bot_eq_one, generalize from Prop to Sort* (#8412)

Estimated changes

Modified src/data/pnat/basic.lean

added theorem pnat.bot_eq_one

deleted theorem pnat.bot_eq_zero

added def pnat.case_strong_induction_on

deleted theorem pnat.case_strong_induction_on

modified theorem pnat.coe_le_coe

modified theorem pnat.coe_lt_coe

modified theorem pnat.exists_eq_succ_of_ne_one

modified theorem pnat.ne_zero

modified def pnat.rec_on

modified theorem pnat.rec_on_succ

added def pnat.strong_induction_on

deleted theorem pnat.strong_induction_on