Commit 2024-11-13 09:53 6567a9b2

View on Github →

feat: add lemmas about instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual (#18787)

Estimated changes

Modified Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

added theorem ofAdd_bot

added theorem ofAdd_toDual_eq_zero_iff

added theorem ofDual_toAdd_eq_top_iff

added theorem ofDual_toAdd_zero