Commit 2022-12-23 12:08 3fe9b592

View on Github →

feat: port Data.PNat.Basic (#1144) Fairly straight forward, with no bigger issues.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/PNat/Basic.lean

added def Equiv.pnatEquivNat

added theorem Nat.succPNat_inj

added theorem Nat.succPNat_injective

added theorem Nat.succPNat_le_succPNat

added theorem Nat.succPNat_lt_succPNat

added theorem Nat.succPNat_mono

added theorem Nat.succPNat_strictMono

added def OrderIso.pnatIsoNat

added theorem OrderIso.pnatIsoNat_symm_apply

added theorem PNat.add_coe

added theorem PNat.add_one_le_iff

added theorem PNat.add_sub_of_lt

added theorem PNat.bit0_le_bit0

added theorem PNat.bit0_le_bit1

added theorem PNat.bit1_le_bit0

added theorem PNat.bit1_le_bit1

added theorem PNat.bot_eq_one

added def PNat.caseStrongInductionOn

added def PNat.coeAddHom

added def PNat.coeMonoidHom

added theorem PNat.coe_bit0

added theorem PNat.coe_bit1

added theorem PNat.coe_coeMonoidHom

added theorem PNat.coe_inj

added theorem PNat.div_add_mod'

added theorem PNat.div_add_mod

added theorem PNat.dvd_antisymm

added theorem PNat.dvd_iff'

added theorem PNat.dvd_iff

added theorem PNat.dvd_one_iff

added theorem PNat.exists_eq_succ_of_ne_one

added theorem PNat.le_of_dvd

added theorem PNat.le_one_iff

added theorem PNat.lt_add_left

added theorem PNat.lt_add_one_iff

added theorem PNat.lt_add_right

added theorem PNat.mk_bit0

added theorem PNat.mk_bit1

added theorem PNat.modDivAux_spec

added theorem PNat.mod_add_div'

added theorem PNat.mod_add_div

added theorem PNat.mod_le

added theorem PNat.mul_coe

added theorem PNat.mul_div_exact

added theorem PNat.natPred_add_one

added theorem PNat.natPred_inj

added theorem PNat.natPred_injective

added theorem PNat.natPred_le_natPred

added theorem PNat.natPred_lt_natPred

added theorem PNat.natPred_monotone

added theorem PNat.natPred_strictMono

added theorem PNat.one_add_natPred

added theorem PNat.pos_of_div_pos

added theorem PNat.pow_coe

added def PNat.recOn

added theorem PNat.recOn_one

added theorem PNat.recOn_succ

added theorem PNat.sub_coe