use R^c

CHANGELOG_UNRELEASED.md

@@ -25,24 +25,6 @@
 
 ### Changed
 
-- in `normedtype.v`:
-  + lemmas `vitali_lemma_finite` and `vitali_lemma_finite_cover` now returns
-    duplicate-free lists of indices
-
-- moved from `lebesgue_integral.v` to `measure.v`:
-  + definition `ae_eq`
-  + lemmas
-	`ae_eq0`,
-	`ae_eq_comp`,
-	`ae_eq_funeposneg`,
-	`ae_eq_refl`,
-	`ae_eq_trans`,
-	`ae_eq_sub`,
-	`ae_eq_mul2r`,
-	`ae_eq_mul2l`,
-	`ae_eq_mul1l`,
-	`ae_eq_abse`
-
 - move from `forms.v` to `mathcomp_extra.v`:
   + structure `revop`
 

classical/mathcomp_extra.v

@@ -605,9 +605,8 @@ End order_min.
 
 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 R^c.
 Canonical rev_mulr {R : ringType} :=
   @RevOp _ _ _ mulr_rev (@GRing.mul R) (fun _ _ => erefl).

theories/derive.v

@@ -832,7 +832,7 @@ HB.instance Definition _ x := GRing.isLinear.Build R R R _ ( *%R x)
   (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.
+Proof. by move=> ? ? ?; rewrite /mulr_rev mulrDr scalerAl. Qed.
 HB.instance Definition _ y := GRing.isLinear.Build R R R _ (mulr_rev y)
   (mulr_rev_is_linear y).