Commit 2026-04-02 11:08 69f3b8d6

View on Github →

feat(Data/ENat): more lemma about WithBot ENat (#36817) In this PR, we add some lemma about WithBot ENat found useful in dimension shifting.

Estimated changes

Modified Mathlib/Algebra/Order/Monoid/WithTop.lean

added theorem WithBot.lt_zero_iff_eq_bot

Modified Mathlib/Data/ENat/Basic.lean

added theorem ENat.WithBot.add_one_le_natCast_iff

added theorem ENat.WithBot.add_one_le_zero_iff

added theorem ENat.WithBot.coe_eq_natCast

added theorem ENat.add_one_le_iff'