Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-02-06 08:29
60855258
View on Github →
feat: port Data.Nat.PartENat (
#1892
) port of data.net.part_enat
Estimated changes
Modified
Mathlib.lean
Modified
Mathlib/Data/ENat/Basic.lean
deleted
def
ENat.ofNat
Created
Mathlib/Data/Nat/PartENat.lean
added
theorem
PartENat.add_eq_top_iff
added
theorem
PartENat.add_one_le_iff_lt
added
theorem
PartENat.add_one_le_of_lt
added
theorem
PartENat.add_top
added
theorem
PartENat.coe_add_get
added
theorem
PartENat.coe_coeHom
added
theorem
PartENat.coe_le_coe
added
theorem
PartENat.coe_le_iff
added
theorem
PartENat.coe_lt_coe
added
theorem
PartENat.coe_lt_iff
added
theorem
PartENat.dom_natCast
added
theorem
PartENat.dom_of_le_natCast
added
theorem
PartENat.dom_of_le_of_dom
added
theorem
PartENat.dom_of_le_some
added
theorem
PartENat.dom_of_lt
added
theorem
PartENat.dom_some
added
theorem
PartENat.eq_top_iff_forall_le
added
theorem
PartENat.eq_top_iff_forall_lt
added
def
PartENat.find
added
theorem
PartENat.find_dom
added
theorem
PartENat.find_eq_top_iff
added
theorem
PartENat.find_get
added
theorem
PartENat.find_le
added
theorem
PartENat.get_add
added
theorem
PartENat.get_eq_iff_eq_coe
added
theorem
PartENat.get_le_get
added
theorem
PartENat.get_natCast'
added
theorem
PartENat.get_natCast
added
theorem
PartENat.get_one
added
theorem
PartENat.get_zero
added
theorem
PartENat.le_coe_iff
added
theorem
PartENat.le_def
added
theorem
PartENat.le_of_lt_add_one
added
theorem
PartENat.lt_add_one
added
theorem
PartENat.lt_add_one_iff_lt
added
theorem
PartENat.lt_coe_iff
added
theorem
PartENat.lt_def
added
theorem
PartENat.lt_find
added
theorem
PartENat.lt_find_iff
added
theorem
PartENat.lt_wf
added
def
PartENat.natCast_AddMonoidHom
added
theorem
PartENat.natCast_get
added
theorem
PartENat.natCast_inj
added
theorem
PartENat.natCast_lt_top
added
theorem
PartENat.natCast_ne_top
added
theorem
PartENat.ne_top_iff
added
theorem
PartENat.ne_top_iff_dom
added
theorem
PartENat.ne_top_of_lt
added
theorem
PartENat.ne_zero_iff
added
theorem
PartENat.not_dom_iff_eq_top
added
theorem
PartENat.not_isMax_natCast
added
def
PartENat.ofENat
added
theorem
PartENat.ofENat_none
added
theorem
PartENat.ofENat_some
added
theorem
PartENat.pos_iff_one_le
added
def
PartENat.some
added
theorem
PartENat.some_eq_natCast
added
def
PartENat.toWithTop
added
theorem
PartENat.toWithTop_add
added
theorem
PartENat.toWithTop_le
added
theorem
PartENat.toWithTop_lt
added
theorem
PartENat.toWithTop_natCast'
added
theorem
PartENat.toWithTop_natCast
added
theorem
PartENat.toWithTop_ofENat
added
theorem
PartENat.toWithTop_some
added
theorem
PartENat.toWithTop_top'
added
theorem
PartENat.toWithTop_top
added
theorem
PartENat.toWithTop_zero'
added
theorem
PartENat.toWithTop_zero
added
theorem
PartENat.top_add
added
theorem
PartENat.top_eq_none
added
theorem
PartENat.withTopEquiv_le
added
theorem
PartENat.withTopEquiv_lt
added
theorem
PartENat.withTopEquiv_natCast
added
theorem
PartENat.withTopEquiv_symm_coe
added
theorem
PartENat.withTopEquiv_symm_le
added
theorem
PartENat.withTopEquiv_symm_lt
added
theorem
PartENat.withTopEquiv_symm_top
added
theorem
PartENat.withTopEquiv_symm_zero
added
theorem
PartENat.withTopEquiv_top
added
theorem
PartENat.withTopEquiv_zero
added
def
PartENat