Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-05 14:09 33df7ecc

View on Github →

feat(data/nat/enat): has_well_founded for enat (#565)

Estimated changes

added theorem enat.coe_ne_bot
added theorem enat.lt_wf
added def enat.to_with_top
added theorem enat.to_with_top_coe'
added theorem enat.to_with_top_coe
added theorem enat.to_with_top_le
added theorem enat.to_with_top_lt
added theorem enat.to_with_top_top'
added theorem enat.to_with_top_top
added theorem enat.to_with_top_zero'
added theorem enat.to_with_top_zero