Theorem ofAdd_bot

Modification history

2026-07-15 16:59
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
chore: delete deprecated declarations to the end of 2025 (#41178) …
Deleted ofAdd_botView on Github →
2024-11-13 09:53
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
feat: add lemmas about `instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual` (#18787)
Added ofAdd_botView on Github →