Commit 2026-11-10 12:28 8409df20

View on Github →

chore(Algebra/Order/Monoid/WithTop): generalize typeclass assumptions (#45803)

Estimated changes

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

added theorem WithBot.lt_one_iff_eq_bot

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

deleted theorem WithBot.lt_zero_iff_eq_bot

Modified Mathlib/Order/SuccPred/ENat.lean

modified theorem ENat.WithBot.add_one_le_zero_iff