Mathlib Changelog
v4
Changelog
About
Github
Theorem
ENat.WithBot.coe_eq_natCast
Modification history
2026-04-02 11:08
Mathlib/Data/ENat/Basic.lean
feat(Data/ENat): more lemma about WithBot ENat (#36817) …
Added
ENat.WithBot.coe_eq_natCast
View on Github →