chore: Move OrderDual action instances to their own file (#8840)

Also add a few missing ones:
* `OrderDual.instSMulWithZero`
* `OrderDual.instMulAction`
* `OrderDual.instMulActionWithZero`
* `OrderDual.instDistribMulAction`

In every case, we prime the originally unprimed/unnamed version.

Mathlib.lean

@@ -373,6 +373,7 @@ import Mathlib.Algebra.Order.Invertible
 import Mathlib.Algebra.Order.Kleene
 import Mathlib.Algebra.Order.LatticeGroup
 import Mathlib.Algebra.Order.Module
+import Mathlib.Algebra.Order.Module.Synonym
 import Mathlib.Algebra.Order.Monoid.Basic
 import Mathlib.Algebra.Order.Monoid.Canonical.Defs
 import Mathlib.Algebra.Order.Monoid.Defs

Mathlib/Algebra/Order/Module/Synonym.lean

@@ -0,0 +1,93 @@
+/-
+Copyright (c) 2021 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import Mathlib.Algebra.Module.Basic
+import Mathlib.Algebra.Order.Pi
+import Mathlib.Algebra.Ring.OrderSynonym
+
+/-!
+# Action instances for `OrderDual`
+
+This file provides instances of algebraic actions for `OrderDual`. Note that the `SMul` instances
+are already defined in `Mathlib.Algebra.Group.OrderSynonym`.
+
+## See also
+
+* `Mathlib.Algebra.Group.OrderSynonym`
+* `Mathlib.Algebra.Ring.OrderSynonym`
+-/
+
+namespace OrderDual
+variable {α β γ : Type*}
+
+instance instSMulWithZero [Zero α] [AddZeroClass β] [SMulWithZero α β] : SMulWithZero αᵒᵈ β where
+  zero_smul := zero_smul α
+  smul_zero := smul_zero (M := α)
+
+instance instSMulWithZero' [Zero α] [AddZeroClass β] [SMulWithZero α β] : SMulWithZero α βᵒᵈ where
+  zero_smul := zero_smul _ (M := β)
+  smul_zero := smul_zero (A := β)
+
+@[to_additive]
+instance instMulAction [Monoid α] [MulAction α β] : MulAction αᵒᵈ β where
+  one_smul := one_smul α
+  mul_smul := mul_smul (α := α)
+
+@[to_additive]
+instance instMulAction' [Monoid α] [MulAction α β] : MulAction α βᵒᵈ where
+  one_smul := one_smul _ (α := β)
+  mul_smul := mul_smul (β := β)
+
+@[to_additive]
+instance instSMulCommClass [SMul β γ] [SMul α γ] [SMulCommClass α β γ] : SMulCommClass αᵒᵈ β γ :=
+   ‹SMulCommClass α β γ›
+
+@[to_additive]
+instance instSMulCommClass' [SMul β γ] [SMul α γ] [SMulCommClass α β γ] : SMulCommClass α βᵒᵈ γ :=
+  ‹SMulCommClass α β γ›
+
+@[to_additive]
+instance instSMulCommClass'' [SMul β γ] [SMul α γ] [SMulCommClass α β γ] : SMulCommClass α β γᵒᵈ :=
+  ‹SMulCommClass α β γ›
+
+@[to_additive instVAddAssocClass]
+instance instIsScalarTower [SMul α β] [SMul β γ] [SMul α γ] [IsScalarTower α β γ] :
+   IsScalarTower αᵒᵈ β γ := ‹IsScalarTower α β γ›
+
+@[to_additive instVAddAssocClass']
+instance instIsScalarTower' [SMul α β] [SMul β γ] [SMul α γ] [IsScalarTower α β γ] :
+    IsScalarTower α βᵒᵈ γ := ‹IsScalarTower α β γ›
+
+@[to_additive instVAddAssocClass'']
+instance instIsScalarTower'' [SMul α β] [SMul β γ] [SMul α γ] [IsScalarTower α β γ] :
+    IsScalarTower α β γᵒᵈ := ‹IsScalarTower α β γ›
+
+instance instMulActionWithZero [MonoidWithZero α] [AddMonoid β] [MulActionWithZero α β] :
+    MulActionWithZero αᵒᵈ β :=
+  { OrderDual.instMulAction, OrderDual.instSMulWithZero with }
+
+instance instMulActionWithZero' [MonoidWithZero α] [AddMonoid β] [MulActionWithZero α β] :
+    MulActionWithZero α βᵒᵈ :=
+  { OrderDual.instMulAction', OrderDual.instSMulWithZero' with }
+
+instance instDistribMulAction [MonoidWithZero α] [AddMonoid β] [DistribMulAction α β] :
+    DistribMulAction αᵒᵈ β where
+  smul_add := smul_add (M := α)
+  smul_zero := smul_zero (M := α)
+
+instance instDistribMulAction' [MonoidWithZero α] [AddMonoid β] [DistribMulAction α β] :
+    DistribMulAction α βᵒᵈ where
+  smul_add := smul_add (A := β)
+  smul_zero := smul_zero (A := β)
+
+instance instModule [Semiring α] [AddCommMonoid β] [Module α β] : Module αᵒᵈ β where
+  add_smul := add_smul (R := α)
+  zero_smul := zero_smul _
+
+instance instModule' [Semiring α] [AddCommMonoid β] [Module α β] : Module α βᵒᵈ where
+  add_smul := add_smul (M := β)
+  zero_smul := zero_smul _
+
+end OrderDual

Mathlib/Algebra/Order/SMul.lean

@@ -5,6 +5,7 @@ Authors: Frédéric Dupuis
 -/
 import Mathlib.Algebra.Module.Pi
 import Mathlib.Algebra.Module.Prod
+import Mathlib.Algebra.Order.Module.Synonym
 import Mathlib.Algebra.Order.Monoid.Prod
 import Mathlib.Algebra.Order.Pi
 import Mathlib.Data.Set.Pointwise.SMul
@@ -55,57 +56,10 @@ class OrderedSMul (R M : Type*) [OrderedSemiring R] [OrderedAddCommMonoid M] [SM
 
 variable {ι α β γ 𝕜 R M N : Type*}
 
-namespace OrderDual
-
-instance OrderDual.instSMulWithZero [Zero R] [AddZeroClass M] [SMulWithZero R M] :
-    SMulWithZero R Mᵒᵈ :=
-  { OrderDual.instSMul with
-    zero_smul := fun m => OrderDual.rec (zero_smul _) m
-    smul_zero := fun r => OrderDual.rec (@smul_zero R M _ _) r }
-
-@[to_additive]
-instance OrderDual.instMulAction [Monoid R] [MulAction R M] : MulAction R Mᵒᵈ :=
-  { OrderDual.instSMul with
-    one_smul := fun m => OrderDual.rec (one_smul _) m
-    mul_smul := fun r => OrderDual.rec (@mul_smul R M _ _) r }
-
-@[to_additive]
-instance OrderDual.instSMulCommClass [SMul β γ] [SMul α γ] [SMulCommClass α β γ] :
-    SMulCommClass αᵒᵈ β γ := ‹SMulCommClass α β γ›
-
-@[to_additive]
-instance OrderDual.instSMulCommClass' [SMul β γ] [SMul α γ] [SMulCommClass α β γ] :
-    SMulCommClass α βᵒᵈ γ := ‹SMulCommClass α β γ›
-
-@[to_additive]
-instance OrderDual.instSMulCommClass'' [SMul β γ] [SMul α γ] [SMulCommClass α β γ] :
-    SMulCommClass α β γᵒᵈ := ‹SMulCommClass α β γ›
-
-@[to_additive OrderDual.instVAddAssocClass]
-instance OrderDual.instIsScalarTower [SMul α β] [SMul β γ] [SMul α γ] [IsScalarTower α β γ] :
-   IsScalarTower αᵒᵈ β γ := ‹IsScalarTower α β γ›
-
-@[to_additive OrderDual.instVAddAssocClass']
-instance OrderDual.instIsScalarTower' [SMul α β] [SMul β γ] [SMul α γ] [IsScalarTower α β γ] :
-    IsScalarTower α βᵒᵈ γ := ‹IsScalarTower α β γ›
-
-@[to_additive OrderDual.instVAddAssocClass'']
-instance OrderDual.IsScalarTower'' [SMul α β] [SMul β γ] [SMul α γ] [IsScalarTower α β γ] :
-    IsScalarTower α β γᵒᵈ := ‹IsScalarTower α β γ›
-
-instance [MonoidWithZero R] [AddMonoid M] [MulActionWithZero R M] : MulActionWithZero R Mᵒᵈ :=
-  { OrderDual.instMulAction, OrderDual.instSMulWithZero with }
-
-instance [MonoidWithZero R] [AddMonoid M] [DistribMulAction R M] : DistribMulAction R Mᵒᵈ where
-  smul_add _ a := OrderDual.rec (fun _ b => OrderDual.rec (smul_add _ _) b) a
-  smul_zero r := OrderDual.rec (@smul_zero _ M _ _) r
-
-instance [OrderedSemiring R] [OrderedAddCommMonoid M] [SMulWithZero R M] [OrderedSMul R M] :
-    OrderedSMul R Mᵒᵈ where
-  smul_lt_smul_of_pos {a b} := @OrderedSMul.smul_lt_smul_of_pos R M _ _ _ _ b a
-  lt_of_smul_lt_smul_of_pos {a b} := @OrderedSMul.lt_of_smul_lt_smul_of_pos R M _ _ _ _ b a
-
-end OrderDual
+instance OrderDual.instOrderedSMul [OrderedSemiring R] [OrderedAddCommMonoid M] [SMulWithZero R M]
+    [OrderedSMul R M] : OrderedSMul R Mᵒᵈ where
+  smul_lt_smul_of_pos := OrderedSMul.smul_lt_smul_of_pos (M := M)
+  lt_of_smul_lt_smul_of_pos := OrderedSMul.lt_of_smul_lt_smul_of_pos (M := M)
 
 section OrderedSMul