Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-30 10:07 5e86589d

View on Github →

chore(data/nat/enat): some useful lemmas (#5517)

Estimated changes

Modified src/data/nat/basic.lean

added theorem nat.find_le

Modified src/data/nat/enat.lean

added theorem enat.coe_le_iff

added theorem enat.coe_lt_iff

added theorem enat.dom_coe

added theorem enat.dom_of_le_of_dom

modified theorem enat.dom_of_le_some

added theorem enat.dom_of_lt

added theorem enat.eq_top_iff_forall_le

added theorem enat.eq_top_iff_forall_lt

added def enat.find

added theorem enat.find_dom

added theorem enat.find_eq_top_iff

added theorem enat.find_get

added theorem enat.find_le

added theorem enat.get_coe'

modified theorem enat.get_coe

modified theorem enat.get_le_get

added theorem enat.le_coe_iff

added theorem enat.le_def

added theorem enat.lt_coe_iff

added theorem enat.lt_def

added theorem enat.lt_find

added theorem enat.lt_find_iff

modified def enat.to_with_top

modified theorem enat.to_with_top_zero'

Modified src/ring_theory/multiplicity.lean

deleted theorem nat.find_le

Modified src/ring_theory/power_series/basic.lean