Theorem WithBot.lt_one_iff_eq_bot

Modification history

2026-11-10 12:28
Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
chore(Algebra/Order/Monoid/WithTop): generalize typeclass assumptions (#45803)
Added WithBot.lt_one_iff_eq_botView on Github →