unfold mulr_rev

math-comp · Apr 17, 2024 · c401207 · c401207
1 parent 555c57c
commit c401207
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 6 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -29,7 +29,6 @@
   + structure `revop`
 
 - move from `derive.v` to `mathcomp_extra.v`:
-  + definition `mulr_rev`
   + canonical `rev_mulr`
 
 ### Renamed
@@ -73,6 +72,9 @@
 - in `lebesgue_integral.v`:
   + `integrablerM`, `integrableMr` (were deprecated since version 0.6.4)
 
+- in `forms.v`:
+  + definition `mulr_rev`
+
 ### Infrastructure
 
 ### Misc
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
@@ -607,6 +607,5 @@ 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 }.
 
-Definition mulr_rev {R : ringType} := @GRing.mul R^c.
 Canonical rev_mulr {R : ringType} :=
-  @RevOp _ _ _ mulr_rev (@GRing.mul R) (fun _ _ => erefl).
+  @RevOp _ _ _ (@GRing.mul R^c) (@GRing.mul R) (fun _ _ => erefl).
diff --git a/theories/derive.v b/theories/derive.v
@@ -831,9 +831,9 @@ Proof. by move=> ? ? ?; rewrite mulrDr scalerAr. Qed.
 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 mulrDr scalerAl. Qed.
-HB.instance Definition _ y := GRing.isLinear.Build R R R _ (mulr_rev y)
+Lemma mulr_rev_is_linear y : linear (@GRing.mul R^c y : R -> R).
+Proof. by move=> ? ? ?; rewrite mulrDr scalerAl. Qed.
+HB.instance Definition _ y := GRing.isLinear.Build R R R _ (@GRing.mul R^c y)
   (mulr_rev_is_linear y).
 
 Lemma mulr_is_bilinear :