Commit 2024-06-23 11:05 a6a6c6ba

View on Github →

chore(Data/ENat): unbundle ENat.toNat (#13936) This will allow us to write n.toNat instead of ENat.toNat n

Estimated changes

Modified Mathlib/Data/ENat/Basic.lean

added theorem ENat.coe_toNatHom

modified def ENat.toNat

added def ENat.toNatHom

added theorem ENat.toNatHom_apply

Modified Mathlib/Data/Set/Card.lean

Modified Mathlib/SetTheory/Cardinal/ToNat.lean