Commit 2025-03-17 19:11 8b1844c4

View on Github →

feat: add lemma ENat.toNat_eq_iff_eq_coe (#23006)

Estimated changes

Modified Mathlib/Data/ENat/Basic.lean

added theorem ENat.toNat_eq_iff_eq_coe

Modified Mathlib/Data/Set/Card.lean