Theorem ofDual_toAdd_eq_top_iff

Modification history

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