Theorem ofAdd_toDual_eq_zero_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 ofAdd_toDual_eq_zero_iffView on Github →
2024-11-13 09:53
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
feat: add lemmas about `instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual` (#18787)
Added ofAdd_toDual_eq_zero_iffView on Github →