chore(algebra/order/{monoid,ring}): missing typeclasses about * and…

… `+` on `order_dual` (#13004)

src/algebra/order/group.lean

@@ -93,6 +93,7 @@ instance ordered_comm_group.has_exists_mul_of_le (α : Type u)
 
 @[to_additive] instance [h : has_inv α] : has_inv (order_dual α) := h
 @[to_additive] instance [h : has_div α] : has_div (order_dual α) := h
+@[to_additive] instance [h : has_involutive_inv α] : has_involutive_inv (order_dual α) := h
 @[to_additive] instance [h : div_inv_monoid α] : div_inv_monoid (order_dual α) := h
 @[to_additive] instance [h : group α] : group (order_dual α) := h
 @[to_additive] instance [h : comm_group α] : comm_group (order_dual α) := h

src/algebra/order/monoid.lean

@@ -915,9 +915,20 @@ namespace order_dual
 
 @[to_additive] instance [h : has_mul α] : has_mul (order_dual α) := h
 @[to_additive] instance [h : has_one α] : has_one (order_dual α) := h
+@[to_additive] instance [h : semigroup α] : semigroup (order_dual α) := h
+@[to_additive] instance [h : comm_semigroup α] : comm_semigroup (order_dual α) := h
+@[to_additive] instance [h : mul_one_class α] : mul_one_class (order_dual α) := h
 @[to_additive] instance [h : monoid α] : monoid (order_dual α) := h
 @[to_additive] instance [h : comm_monoid α] : comm_monoid (order_dual α) := h
+@[to_additive] instance [h : left_cancel_monoid α] : left_cancel_monoid (order_dual α) := h
+@[to_additive] instance [h : right_cancel_monoid α] : right_cancel_monoid (order_dual α) := h
+@[to_additive] instance [h : cancel_monoid α] : cancel_monoid (order_dual α) := h
 @[to_additive] instance [h : cancel_comm_monoid α] : cancel_comm_monoid (order_dual α) := h
+instance [h : mul_zero_class α] : mul_zero_class (order_dual α) := h
+instance [h : mul_zero_one_class α] : mul_zero_one_class (order_dual α) := h
+instance [h : monoid_with_zero α] : monoid_with_zero (order_dual α) := h
+instance [h : comm_monoid_with_zero α] : comm_monoid_with_zero (order_dual α) := h
+instance [h : cancel_comm_monoid_with_zero α] : cancel_comm_monoid_with_zero (order_dual α) := h
 
 @[to_additive]
 instance contravariant_class_mul_le [has_le α] [has_mul α] [c : contravariant_class α α (*) (≤)] :

src/algebra/order/ring.lean

@@ -90,6 +90,26 @@ set_option old_structure_cmd true
 universe u
 variable {α : Type u}
 
+namespace order_dual
+
+/-! Note that `order_dual` does not satisfy any of the ordered ring typeclasses due to the
+`zero_le_one` field. -/
+
+instance [h : distrib α] : distrib (order_dual α) := h
+instance [has_mul α] [h : has_distrib_neg α] : has_distrib_neg (order_dual α) := h
+instance [h : non_unital_non_assoc_semiring α] : non_unital_non_assoc_semiring (order_dual α) := h
+instance [h : non_unital_semiring α] : non_unital_semiring (order_dual α) := h
+instance [h : non_assoc_semiring α] : non_assoc_semiring (order_dual α) := h
+instance [h : semiring α] : semiring (order_dual α) := h
+instance [h : comm_semiring α] : comm_semiring (order_dual α) := h
+instance [h : non_unital_non_assoc_ring α] : non_unital_non_assoc_ring (order_dual α) := h
+instance [h : non_unital_ring α] : non_unital_ring (order_dual α) := h
+instance [h : non_assoc_ring α] : non_assoc_ring (order_dual α) := h
+instance [h : ring α] : ring (order_dual α) := h
+instance [h : comm_ring α] : comm_ring (order_dual α) := h
+
+end order_dual
+
 lemma add_one_le_two_mul [has_le α] [semiring α] [covariant_class α α (+) (≤)]
   {a : α} (a1 : 1 ≤ a) :
   a + 1 ≤ 2 * a :=