rm mulr_rev stuff

math-comp · Apr 24, 2024 · c889b05 · c889b05
1 parent 59db8ff
commit c889b05
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 14 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -39,6 +39,9 @@
 - move from `derive.v` to `mathcomp_extra.v`:
   + canonical `rev_mulr`
 
+- in `forms.v`:
+  + notation ``` u ``_ _ ````
+
 ### Renamed
 
 - in `constructive_ereal.v`:
@@ -98,8 +101,12 @@
 - in `measure.v`:
   + lemmas `prod_salgebra_set0`, `prod_salgebra_setC`, `prod_salgebra_bigcup`
     (use `measurable0`, `measurableC`, `measurable_bigcup` instead)
-- in `forms.v`:
+- in `derive.v`:
   + definition `mulr_rev`
+  + canonical `rev_mulr`
+  + lemmas `mulr_is_linear`, `mulr_rev_is_linear`
+- in `forms.v`:
+  + structure `revop`
 
 ### Infrastructure
 

diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
@@ -613,9 +613,9 @@ Qed.
 
 End order_min.
 
-Structure revop X Y Z (f : Y -> X -> Z) := RevOp {
+(*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 }.
 
 Canonical rev_mulr {R : ringType} :=
-  @RevOp _ _ _ (@GRing.mul R^c) (@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
@@ -826,16 +826,6 @@ Proof.
 by move=> fc; apply/diff_locallyP; rewrite diff_bilin //; apply: dbilin p fc.
 Qed.
 
-Lemma mulr_is_linear x : linear (@GRing.mul R x : R -> R).
-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 (@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 :
   bilinear_for
     (GRing.Scale.Law.clone _ _ *:%R _) (GRing.Scale.Law.clone _ _ *:%R _)

diff --git a/theories/forms.v b/theories/forms.v
@@ -27,7 +27,7 @@ Reserved Notation "A ^_|_"    (at level 8, format "A ^_|_").
 Reserved Notation "A _|_ B" (at level 69, format "A  _|_  B").
 Reserved Notation "eps_theta .-sesqui" (at level 2, format "eps_theta .-sesqui").
 
-Notation "u '``_' i" := (u (GRing.zero [the zmodType of 'I_1]) i) : ring_scope.
+Notation "u '``_' i" := (u (0 : 'I_1) i) : ring_scope.
 Notation "''e_' i" := (delta_mx 0 i)
  (format "''e_' i", at level 3) : ring_scope.