Theorem Cardinal.toENat_lt_natCast

Modification history

2026-02-23 18:16

Mathlib/SetTheory/Cardinal/ENat.lean

feat(SetTheory/Cardinal): more lemmas about `ENat` (#33909) …

Added Cardinal.toENat_lt_natCast View on Github →