chore(Algebra/TrivSqZeroExt): use open scoped RightActions (leanpro…

…ver-community#10546)

One lemma statement has changed (up to associativity).

This is one of the more compelling justifications for leanprover-community#8909.

Mathlib/Algebra/TrivSqZeroExt.lean

@@ -44,7 +44,7 @@ Many of the later results in this file are only stated for the commutative `R'`
   morphisms `TrivSqZeroExt R M →ₐ[S] A` are uniquely defined by an algebra morphism `f : R →ₐ[S] A`
   on `R` and a linear map `g : M →ₗ[S] A` on `M` such that:
   * `g x * g y = 0`: the elements of `M` continue to square to zero.
-  * `g (r • x) = f r * g x` and `g (op r • x) = g x * f r`: left and right actions are preserved by
+  * `g (r •> x) = f r * g x` and `g (x <• r) = g x * f r`: left and right actions are preserved by
     `g`.
 * `TrivSqZeroExt.lift`: the universal property of the trivial square-zero extension; algebra
   morphisms `TrivSqZeroExt R M →ₐ[R] A` are uniquely defined by linear maps `M →ₗ[R] A` for
@@ -69,11 +69,11 @@ def TrivSqZeroExt (R : Type u) (M : Type v) :=
 -- mathport name: exprtsze
 local notation "tsze" => TrivSqZeroExt
 
-open BigOperators
+open scoped BigOperators RightActions
 
 namespace TrivSqZeroExt
 
-open MulOpposite (op)
+open MulOpposite
 
 section Basic
 
@@ -434,7 +434,7 @@ instance one [One R] [Zero M] : One (tsze R M) :=
   ⟨(1, 0)⟩
 
 instance mul [Mul R] [Add M] [SMul R M] [SMul Rᵐᵒᵖ M] : Mul (tsze R M) :=
-  ⟨fun x y => (x.1 * y.1, x.1 • y.2 + op y.1 • x.2)⟩
+  ⟨fun x y => (x.1 * y.1, x.1 •> y.2 + x.2 <• y.1)⟩
 
 @[simp]
 theorem fst_one [One R] [Zero M] : (1 : tsze R M).fst = 1 :=
@@ -454,7 +454,7 @@ theorem fst_mul [Mul R] [Add M] [SMul R M] [SMul Rᵐᵒᵖ M] (x₁ x₂ : tsze
 
 @[simp]
 theorem snd_mul [Mul R] [Add M] [SMul R M] [SMul Rᵐᵒᵖ M] (x₁ x₂ : tsze R M) :
-    (x₁ * x₂).snd = x₁.fst • x₂.snd + op x₂.fst • x₁.snd :=
+    (x₁ * x₂).snd = x₁.fst •> x₂.snd + x₁.snd <• x₂.fst :=
   rfl
 #align triv_sq_zero_ext.snd_mul TrivSqZeroExt.snd_mul
 
@@ -470,7 +470,7 @@ theorem inl_one [One R] [Zero M] : (inl 1 : tsze R M) = 1 :=
 @[simp]
 theorem inl_mul [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M]
     (r₁ r₂ : R) : (inl (r₁ * r₂) : tsze R M) = inl r₁ * inl r₂ :=
-  ext rfl <| show (0 : M) = r₁ • (0 : M) + op r₂ • (0 : M) by rw [smul_zero, zero_add, smul_zero]
+  ext rfl <| show (0 : M) = r₁ •> (0 : M) + (0 : M) <• r₂ by rw [smul_zero, zero_add, smul_zero]
 #align triv_sq_zero_ext.inl_mul TrivSqZeroExt.inl_mul
 
 theorem inl_mul_inl [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M]
@@ -488,7 +488,7 @@ variable (R)
 theorem inr_mul_inr [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] (m₁ m₂ : M) :
     (inr m₁ * inr m₂ : tsze R M) = 0 :=
   ext (mul_zero _) <|
-    show (0 : R) • m₂ + (0 : Rᵐᵒᵖ) • m₁ = 0 by rw [zero_smul, zero_add, zero_smul]
+    show (0 : R) •> m₂ + m₁ <• (0 : R) = 0 by rw [zero_smul, zero_add, op_zero, zero_smul]
 #align triv_sq_zero_ext.inr_mul_inr TrivSqZeroExt.inr_mul_inr
 
 end
@@ -500,30 +500,30 @@ theorem inl_mul_inr [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒ
 #align triv_sq_zero_ext.inl_mul_inr TrivSqZeroExt.inl_mul_inr
 
 theorem inr_mul_inl [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] (r : R) (m : M) :
-    (inr m * inl r : tsze R M) = inr (op r • m) :=
+    (inr m * inl r : tsze R M) = inr (m <• r) :=
   ext (zero_mul r) <|
-    show (0 : R) • (0 : M) + op r • m = op r • m by rw [smul_zero, zero_add]
+    show (0 : R) •> (0 : M) + m <• r = m <• r by rw [smul_zero, zero_add]
 #align triv_sq_zero_ext.inr_mul_inl TrivSqZeroExt.inr_mul_inl
 
 theorem inl_mul_eq_smul [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M]
     (r : R) (x : tsze R M) :
-    inl r * x = r • x :=
+    inl r * x = r •> x :=
   ext rfl (by dsimp; rw [smul_zero, add_zero])
 
 theorem mul_inl_eq_op_smul [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M]
     (x : tsze R M) (r : R) :
-    x * inl r = op r • x :=
+    x * inl r = x <• r :=
   ext rfl (by dsimp; rw [smul_zero, zero_add])
 
 instance mulOneClass [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] :
     MulOneClass (tsze R M) :=
   { TrivSqZeroExt.one, TrivSqZeroExt.mul with
     one_mul := fun x =>
       ext (one_mul x.1) <|
-        show (1 : R) • x.2 + op x.1 • (0 : M) = x.2 by rw [one_smul, smul_zero, add_zero]
+        show (1 : R) •> x.2 + (0 : M) <• x.1 = x.2 by rw [one_smul, smul_zero, add_zero]
     mul_one := fun x =>
       ext (mul_one x.1) <|
-        show x.1 • (0 : M) + (1 : Rᵐᵒᵖ) • x.2 = x.2 by rw [smul_zero, zero_add, one_smul] }
+        show x.1 • (0 : M) + x.2 <• (1 : R) = x.2 by rw [smul_zero, zero_add, op_one, one_smul] }
 
 instance addMonoidWithOne [AddMonoidWithOne R] [AddMonoid M] : AddMonoidWithOne (tsze R M) :=
   { TrivSqZeroExt.addMonoid, TrivSqZeroExt.one with
@@ -572,21 +572,21 @@ instance nonAssocSemiring [Semiring R] [AddCommMonoid M] [Module R M] [Module R
   { TrivSqZeroExt.addMonoidWithOne, TrivSqZeroExt.mulOneClass, TrivSqZeroExt.addCommMonoid with
     zero_mul := fun x =>
       ext (zero_mul x.1) <|
-        show (0 : R) • x.2 + op x.1 • (0 : M) = 0 by rw [zero_smul, zero_add, smul_zero]
+        show (0 : R) •> x.2 + (0 : M) <• x.1 = 0 by rw [zero_smul, zero_add, smul_zero]
     mul_zero := fun x =>
       ext (mul_zero x.1) <|
         show x.1 • (0 : M) + (0 : Rᵐᵒᵖ) • x.2 = 0 by rw [smul_zero, zero_add, zero_smul]
     left_distrib := fun x₁ x₂ x₃ =>
       ext (mul_add x₁.1 x₂.1 x₃.1) <|
         show
-          x₁.1 • (x₂.2 + x₃.2) + (op x₂.1 + op x₃.1) • x₁.2 =
-            x₁.1 • x₂.2 + op x₂.1 • x₁.2 + (x₁.1 • x₃.2 + op x₃.1 • x₁.2)
-          by simp_rw [smul_add, add_smul, add_add_add_comm]
+          x₁.1 •> (x₂.2 + x₃.2) + x₁.2 <• (x₂.1 + x₃.1) =
+            x₁.1 •> x₂.2 + x₁.2 <• x₂.1 + (x₁.1 •> x₃.2 + x₁.2 <• x₃.1)
+          by simp_rw [smul_add, MulOpposite.op_add, add_smul, add_add_add_comm]
     right_distrib := fun x₁ x₂ x₃ =>
       ext (add_mul x₁.1 x₂.1 x₃.1) <|
         show
-          (x₁.1 + x₂.1) • x₃.2 + op x₃.1 • (x₁.2 + x₂.2) =
-            x₁.1 • x₃.2 + op x₃.1 • x₁.2 + (x₂.1 • x₃.2 + op x₃.1 • x₂.2)
+          (x₁.1 + x₂.1) •> x₃.2 + (x₁.2 + x₂.2) <• x₃.1 =
+            x₁.1 •> x₃.2 + x₁.2 <• x₃.1 + (x₂.1 •> x₃.2 + x₂.2 <• x₃.1)
           by simp_rw [add_smul, smul_add, add_add_add_comm] }
 
 instance nonAssocRing [Ring R] [AddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] :
@@ -605,7 +605,7 @@ In the commutative case this becomes the simpler $(r + m)^n = r^n + nr^{n-1}m$.
 instance [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] :
     Pow (tsze R M) ℕ :=
   ⟨fun x n =>
-    ⟨x.fst ^ n, ((List.range n).map fun i => x.fst ^ (n.pred - i) • op (x.fst ^ i) • x.snd).sum⟩⟩
+    ⟨x.fst ^ n, ((List.range n).map fun i => x.fst ^ (n.pred - i) •> x.snd <• x.fst ^ i).sum⟩⟩
 
 @[simp]
 theorem fst_pow [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M]
@@ -615,20 +615,14 @@ theorem fst_pow [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulActio
 
 theorem snd_pow_eq_sum [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M]
     (x : tsze R M) (n : ℕ) :
-    snd (x ^ n) = ((List.range n).map fun i => x.fst ^ (n.pred - i) • op (x.fst ^ i) • x.snd).sum :=
+    snd (x ^ n) = ((List.range n).map fun i => x.fst ^ (n.pred - i) •> x.snd <• x.fst ^ i).sum :=
   rfl
 #align triv_sq_zero_ext.snd_pow_eq_sum TrivSqZeroExt.snd_pow_eq_sum
 
 theorem snd_pow_of_smul_comm [Monoid R] [AddMonoid M] [DistribMulAction R M]
     [DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (x : tsze R M) (n : ℕ)
-    (h : op x.fst • x.snd = x.fst • x.snd) : snd (x ^ n) = n • x.fst ^ n.pred • x.snd := by
-  have : ∀ n : ℕ, op (x.fst ^ n) • x.snd = x.fst ^ n • x.snd := by
-    intro n
-    induction' n with n ih
-    · simp
-    · rw [pow_succ', MulOpposite.op_mul, mul_smul, mul_smul, ← h,
-        smul_comm (_ : R) (op x.fst) x.snd, ih]
-  simp_rw [snd_pow_eq_sum, this, smul_smul, ← pow_add]
+    (h : x.snd <• x.fst = x.fst •> x.snd) : snd (x ^ n) = n • x.fst ^ n.pred •> x.snd := by
+  simp_rw [snd_pow_eq_sum, ← smul_comm (_ : R) (_ : Rᵐᵒᵖ), aux, smul_smul, ← pow_add]
   match n with
   | 0 => rw [Nat.pred_zero, pow_zero, List.range_zero, zero_smul, List.map_nil, List.sum_nil]
   | (Nat.succ n) =>
@@ -639,8 +633,19 @@ theorem snd_pow_of_smul_comm [Monoid R] [AddMonoid M] [DistribMulAction R M]
       obtain ⟨i, hi, rfl⟩ := hm
       rw [tsub_add_cancel_of_le (Nat.lt_succ_iff.mp hi)]
     · rw [List.length_map, List.length_range]
+where
+  aux : ∀ n : ℕ, x.snd <• x.fst ^ n = x.fst ^ n •> x.snd := by
+    intro n
+    induction' n with n ih
+    · simp
+    · rw [pow_succ', op_mul, mul_smul, mul_smul, ← h, smul_comm (_ : R) (op x.fst) x.snd, ih]
 #align triv_sq_zero_ext.snd_pow_of_smul_comm TrivSqZeroExt.snd_pow_of_smul_comm
 
+theorem snd_pow_of_smul_comm' [Monoid R] [AddMonoid M] [DistribMulAction R M]
+    [DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (x : tsze R M) (n : ℕ)
+    (h : x.snd <• x.fst = x.fst •> x.snd) : snd (x ^ n) = n • (x.snd <• x.fst ^ n.pred) := by
+  rw [snd_pow_of_smul_comm _ _ h, snd_pow_of_smul_comm.aux _ h]
+
 @[simp]
 theorem snd_pow [CommMonoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M]
     [IsCentralScalar R M] (x : tsze R M) (n : ℕ) : snd (x ^ n) = n • x.fst ^ n.pred • x.snd :=
@@ -659,9 +664,9 @@ instance monoid [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulActio
     mul_assoc := fun x y z =>
       ext (mul_assoc x.1 y.1 z.1) <|
         show
-          (x.1 * y.1) • z.2 + op z.1 • (x.1 • y.2 + op y.1 • x.2) =
-            x.1 • (y.1 • z.2 + op z.1 • y.2) + (op z.1 * op y.1) • x.2
-          by simp_rw [smul_add, ← mul_smul, add_assoc, smul_comm]
+          (x.1 * y.1) •> z.2 + (x.1 •> y.2 + x.2 <• y.1) <• z.1 =
+            x.1 •> (y.1 •> z.2 + y.2 <• z.1) + x.2 <• (y.1 * z.1)
+          by simp_rw [smul_add, ← mul_smul, add_assoc, smul_comm, op_mul]
     npow := fun n x => x ^ n
     npow_zero := fun x => ext (pow_zero x.fst) (by simp [snd_pow_eq_sum])
     npow_succ := fun n x =>
@@ -673,12 +678,13 @@ instance monoid [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulActio
           simp_rw [Nat.pred_succ]
           rw [List.range_succ, List.map_append, List.sum_append, List.map_singleton,
             List.sum_singleton, Nat.sub_self, pow_zero, one_smul, List.smul_sum, List.map_map,
-            fst_pow]  --porting note: `Function.comp` no longer works in `rw` so move to `simp_rw`
-          simp_rw [Function.comp, smul_smul, ← pow_succ, Nat.succ_eq_add_one]
+            fst_pow, Function.comp]
+          simp_rw [← smul_comm (_ : R) (_ : Rᵐᵒᵖ), smul_smul, ← pow_succ, Nat.succ_eq_add_one]
           congr 2
           refine' List.map_congr fun i hi => _
           rw [List.mem_range, Nat.lt_succ_iff] at hi
           rw [Nat.sub_add_comm hi]) }
+
 theorem fst_list_prod [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M]
     [SMulCommClass R Rᵐᵒᵖ M] (l : List (tsze R M)) : l.prod.fst = (l.map fst).prod :=
   map_list_prod ({ toFun := fst, map_one' := fst_one, map_mul' := fst_mul } : tsze R M →* R) _
@@ -694,13 +700,14 @@ theorem snd_list_prod [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐ
     [SMulCommClass R Rᵐᵒᵖ M] (l : List (tsze R M)) :
     l.prod.snd =
       (l.enum.map fun x : ℕ × tsze R M =>
-          ((l.map fst).take x.1).prod • op ((l.map fst).drop x.1.succ).prod • x.snd.snd).sum := by
+          ((l.map fst).take x.1).prod •> x.snd.snd <• ((l.map fst).drop x.1.succ).prod).sum := by
   induction' l with x xs ih
   · simp
   · rw [List.enum_cons, ← List.map_fst_add_enum_eq_enumFrom]
     simp_rw [List.map_cons, List.map_map, Function.comp, Prod.map_snd, Prod.map_fst, id,
       List.take_zero, List.take_cons, List.prod_nil, List.prod_cons, snd_mul, one_smul, List.drop,
-      mul_smul, List.sum_cons, fst_list_prod, ih, List.smul_sum, List.map_map]
+      mul_smul, List.sum_cons, fst_list_prod, ih, List.smul_sum, List.map_map,
+      ← smul_comm (_ : R) (_ : Rᵐᵒᵖ)]
     exact add_comm _ _
 #align triv_sq_zero_ext.snd_list_prod TrivSqZeroExt.snd_list_prod
 
@@ -713,7 +720,7 @@ instance commMonoid [CommMonoid R] [AddCommMonoid M] [DistribMulAction R M]
   { TrivSqZeroExt.monoid with
     mul_comm := fun x₁ x₂ =>
       ext (mul_comm x₁.1 x₂.1) <|
-        show x₁.1 • x₂.2 + op x₂.1 • x₁.2 = x₂.1 • x₁.2 + op x₁.1 • x₂.2 by
+        show x₁.1 •> x₂.2 + x₁.2 <• x₂.1 = x₂.1 •> x₁.2 + x₂.2 <• x₁.1 by
           rw [op_smul_eq_smul, op_smul_eq_smul, add_comm] }
 
 instance commSemiring [CommSemiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M]
@@ -757,14 +764,14 @@ instance algebra' : Algebra S (tsze R M) :=
     smul := (· • ·)
     commutes' := fun s x =>
       ext (Algebra.commutes _ _) <|
-        show algebraMap S R s • x.snd + op x.fst • (0 : M)
-            = x.fst • (0 : M) + op (algebraMap S R s) • x.snd by
+        show algebraMap S R s •> x.snd + (0 : M) <• x.fst
+            = x.fst •> (0 : M) + x.snd <• algebraMap S R s by
           rw [smul_zero, smul_zero, add_zero, zero_add]
-          rw [Algebra.algebraMap_eq_smul_one, MulOpposite.op_smul, MulOpposite.op_one, smul_assoc,
+          rw [Algebra.algebraMap_eq_smul_one, MulOpposite.op_smul, op_one, smul_assoc,
             one_smul, smul_assoc, one_smul]
-    smul_def' := fun r x =>
+    smul_def' := fun s x =>
       ext (Algebra.smul_def _ _) <|
-        show r • x.2 = algebraMap S R r • x.2 + op x.1 • (0 : M) by
+        show s • x.snd = algebraMap S R s •> x.snd + (0 : M) <• x.fst by
           rw [smul_zero, add_zero, algebraMap_smul] }
 #align triv_sq_zero_ext.algebra' TrivSqZeroExt.algebra'
 
@@ -831,7 +838,7 @@ Namely, we require that for an algebra morphism `f : R →ₐ[S] A` and a linear
 we have:
 
 * `g x * g y = 0`: the elements of `M` continue to square to zero.
-* `g (r • x) = f r * g x` and `g (op r • x) = g x * f r`: scalar multiplication on the left and
+* `g (r •> x) = f r * g x` and `g (x <• r) = g x * f r`: scalar multiplication on the left and
   right is sent to left- and right- multiplication by the image under `f`.
 
 See `TrivSqZeroExt.liftEquiv` for this as an equiv; namely that any such algebra morphism can be
@@ -841,8 +848,8 @@ When `R` is commutative, this can be invoked with `f = Algebra.ofId R A`, which
 `hgf`. This version is captured as an equiv by `TrivSqZeroExt.liftEquivOfComm`. -/
 def lift (f : R →ₐ[S] A) (g : M →ₗ[S] A)
     (hg : ∀ x y, g x * g y = 0)
-    (hfg : ∀ r x, g (r • x) = f r * g x)
-    (hgf : ∀ r x, g (op r • x) = g x * f r) : tsze R M →ₐ[S] A :=
+    (hfg : ∀ r x, g (r •> x) = f r * g x)
+    (hgf : ∀ r x, g (x <• r) = g x * f r) : tsze R M →ₐ[S] A :=
   AlgHom.ofLinearMap
     ((f.comp <| fstHom S R M).toLinearMap + g ∘ₗ (sndHom R M |>.restrictScalars S))
     (show f 1 + g (0 : M) = 1 by rw [map_zero, map_one, add_zero])
@@ -864,17 +871,17 @@ theorem lift_def (f : R →ₐ[S] A) (g : M →ₗ[S] A)
 @[simp]
 theorem lift_apply_inl (f : R →ₐ[S] A) (g : M →ₗ[S] A)
     (hg : ∀ x y, g x * g y = 0)
-    (hfg : ∀ r x, g (r • x) = f r * g x)
-    (hgf : ∀ r x, g (op r • x) = g x * f r)
+    (hfg : ∀ r x, g (r •> x) = f r * g x)
+    (hgf : ∀ r x, g (x <• r) = g x * f r)
     (r : R) :
     lift f g hg hfg hgf (inl r) = f r :=
   show f r + g 0 = f r by rw [map_zero, add_zero]
 
 @[simp]
 theorem lift_apply_inr (f : R →ₐ[S] A) (g : M →ₗ[S] A)
     (hg : ∀ x y, g x * g y = 0)
-    (hfg : ∀ r x, g (r • x) = f r * g x)
-    (hgf : ∀ r x, g (op r • x) = g x * f r)
+    (hfg : ∀ r x, g (r •> x) = f r * g x)
+    (hgf : ∀ r x, g (x <• r) = g x * f r)
     (m : M) :
     lift f g hg hfg hgf (inr m) = g m :=
   show f 0 + g m = g m by rw [map_zero, zero_add]
@@ -883,16 +890,16 @@ theorem lift_apply_inr (f : R →ₐ[S] A) (g : M →ₗ[S] A)
 @[simp]
 theorem lift_comp_inlHom (f : R →ₐ[S] A) (g : M →ₗ[S] A)
     (hg : ∀ x y, g x * g y = 0)
-    (hfg : ∀ r x, g (r • x) = f r * g x)
-    (hgf : ∀ r x, g (op r • x) = g x * f r) :
+    (hfg : ∀ r x, g (r •> x) = f r * g x)
+    (hgf : ∀ r x, g (x <• r) = g x * f r) :
     (lift f g hg hfg hgf).comp (inlAlgHom S R M) = f :=
   AlgHom.ext <| lift_apply_inl f g hg hfg hgf
 
 @[simp]
 theorem lift_comp_inrHom (f : R →ₐ[S] A) (g : M →ₗ[S] A)
     (hg : ∀ x y, g x * g y = 0)
-    (hfg : ∀ r x, g (r • x) = f r * g x)
-    (hgf : ∀ r x, g (op r • x) = g x * f r) :
+    (hfg : ∀ r x, g (r •> x) = f r * g x)
+    (hgf : ∀ r x, g (x <• r) = g x * f r) :
     (lift f g hg hfg hgf).toLinearMap.comp (inrHom R M |>.restrictScalars S) = g :=
   LinearMap.ext <| lift_apply_inr f g hg hfg hgf
 #align triv_sq_zero_ext.lift_aux_comp_inr_hom TrivSqZeroExt.lift_comp_inrHom
@@ -916,8 +923,8 @@ This isomorphism is named to match the very similar `Complex.lift`. -/
 def liftEquiv :
     {fg : (R →ₐ[S] A) × (M →ₗ[S] A) //
       (∀ x y, fg.2 x * fg.2 y = 0) ∧
-      (∀ r x, fg.2 (r • x) = fg.1 r * fg.2 x) ∧
-      (∀ r x, fg.2 (op r • x) = fg.2 x * fg.1 r)} ≃ (tsze R M →ₐ[S] A) where
+      (∀ r x, fg.2 (r •> x) = fg.1 r * fg.2 x) ∧
+      (∀ r x, fg.2 (x <• r) = fg.2 x * fg.1 r)} ≃ (tsze R M →ₐ[S] A) where
   toFun fg := lift fg.val.1 fg.val.2 fg.prop.1 fg.prop.2.1 fg.prop.2.2
   invFun F :=
     ⟨(F.comp (inlAlgHom _ _ _), F.toLinearMap ∘ₗ (inrHom _ _ |>.restrictScalars _)),