Theorem bot_eq_zero''

Modification history

2026-05-06 19:54
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
feat: `IsBotOneClass` and `IsBotZeroClass` (#38730) …
Deleted bot_eq_zero''View on Github →
2025-01-24 22:55
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
refactor: make `LinearOrderedCommMonoidWithZero` extend `OrderBot` (#19193) …
Added bot_eq_zero''View on Github →