Commit 2025-12-08 18:18 e9bc3ca6

View on Github →

chore: deprecate ENat.not_lt_zero in favor of not_lt_zero (#32381)

Estimated changes

Modified Mathlib/Data/ENat/Basic.lean

deleted theorem ENat.not_lt_zero