Commit 2024-02-14 06:30 5cc14ef3

View on Github →

feat(ENat): add several lemmas (#10508) Add lemmas needed for #10472

Estimated changes

Modified Mathlib/Data/ENat/Basic.lean

added theorem ENat.toNat_eq_zero

Modified Mathlib/SetTheory/Cardinal/ENat.lean

added theorem Cardinal.toENatAux_le_nat

added theorem Cardinal.toENat_le_nat

added theorem Cardinal.toENat_le_ofNat

added theorem Cardinal.toENat_le_one

added theorem Cardinal.toENat_lift