use R^c

math-comp · Jan 1, 2024 · 3c95c57 · 3c95c57
1 parent b76390d
commit 3c95c57
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 5 deletions.
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
@@ -1488,9 +1488,8 @@ Qed.
 
 Structure revop X Y Z (f : Y -> X -> Z) := RevOp {
   fun_of_revop :> X -> Y -> Z;
-  _ : forall x, f x =1 fun_of_revop^~ x
-}.
+  _ : forall x, f x =1 fun_of_revop^~ x }.
 
-Definition mulr_rev {R : ringType} (y x : R) := x * y.
+Definition mulr_rev {R : ringType} := @GRing.mul [ringType of R^c].
 Canonical rev_mulr {R : ringType} :=
   @RevOp _ _ _ mulr_rev (@GRing.mul [ringType of R]) (fun _ _ => erefl).
diff --git a/theories/derive.v b/theories/derive.v
@@ -812,8 +812,8 @@ Lemma mulr_is_linear x : linear (@GRing.mul [ringType of R] x : R -> R).
 Proof. by move=> ???; rewrite mulrDr scalerAr. Qed.
 Canonical mulr_linear x := Linear (mulr_is_linear x).
 
-Lemma mulr_rev_is_linear y : linear (mulr_rev y : R -> R).
-Proof. by move=> ???; rewrite /mulr_rev mulrDl scalerAl. Qed.
+Lemma mulr_rev_is_linear (y : R) : linear (mulr_rev y).
+Proof. by move=> x a b; rewrite /mulr_rev /GRing.mul/= mulrDl scalerAl. Qed.
 Canonical mulr_rev_linear y := Linear (mulr_rev_is_linear y).
 
 Canonical mulr_bilinear :=