Commit 2023-02-06 08:29 60855258

View on Github →

feat: port Data.Nat.PartENat (#1892) port of data.net.part_enat

Estimated changes

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_lt
added theorem PartENat.dom_some
added def PartENat.find
added theorem PartENat.find_dom
added theorem PartENat.find_get
added theorem PartENat.find_le
added theorem PartENat.get_add
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.lt_add_one
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 theorem PartENat.natCast_get
added theorem PartENat.natCast_inj
added theorem PartENat.ne_top_iff
added theorem PartENat.ne_top_of_lt
added theorem PartENat.ne_zero_iff
added def PartENat.ofENat
added theorem PartENat.ofENat_none
added theorem PartENat.ofENat_some
added def PartENat.some
added theorem PartENat.toWithTop_add
added theorem PartENat.toWithTop_le
added theorem PartENat.toWithTop_lt
added theorem PartENat.toWithTop_top
added theorem PartENat.top_add
added theorem PartENat.top_eq_none
added def PartENat