Commit 2026-09-07 10:31 b89e536f

View on Github →

chore(Data/ENat): move ENat.toNat theorems to Basic.lean (#43150) This let's us use them with less imports.

Estimated changes

Modified Mathlib/Data/ENat/Basic.lean

added theorem ENat.natCast_toNat_eq_self

added theorem ENat.toNat_eq_iff

added theorem ENat.toNat_eq_iff_eq_natCast

added theorem ENat.toNat_le_of_le_natCast

added theorem ENat.toNat_le_toNat

Modified Mathlib/Data/ENat/Monoid.lean

deleted theorem ENat.natCast_toNat_eq_self

deleted theorem ENat.toNat_eq_iff

deleted theorem ENat.toNat_eq_iff_eq_natCast

deleted theorem ENat.toNat_le_of_le_natCast

deleted theorem ENat.toNat_le_toNat