Theorem ofDual_toAdd_zero

Modification history

2024-11-13 09:53

Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

feat: add lemmas about `instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual` (#18787)

Added ofDual_toAdd_zero View on Github →