trying to green CI

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -106,7 +106,6 @@
 - in `mathcomp_extra.v`:
   + lemmas `divDl_ge0`, `divDl_le1`
   + mixin `Zmodule_isSubNormed`
-  + structure `SubNormedZmodule`, notation `subNormedZmodType`
 
 - in `unstable.v`:
   + lemmas `divD_onem`

classical/mathcomp_extra.v

@@ -112,15 +112,3 @@ Proof.
 move: s0; rewrite le0r => /predU1P [->|s0]; first by rewrite mul0r.
 by rewrite ler_pdivrMr ?mul1r ?lerDl // ltr_wpDr.
 Qed.
-
-HB.mixin Record Zmodule_isSubNormed (R : numDomainType)
-    (M : normedZmodType R) (S : pred M) T & SubChoice M S T
-    & Num.NormedZmodule R T := {
-  norm_valE : forall x , @Num.norm _ M ((val : T -> M) x) = @Num.norm _ T x
-}.
-
-#[short(type="subNormedZmodType")]
-HB.structure Definition SubNormedZmodule (R : numDomainType)
-    (V : normedZmodType R) (S : pred V) :=
-  { U of SubChoice V S U & Num.NormedZmodule R U & GRing.SubZmodule V S U
-    & Zmodule_isSubNormed R V S U }.

theories/functional_analysis/hahn_banach_theorem.v

@@ -40,6 +40,27 @@ Local Open Scope ring_scope.
 Local Open Scope convex_scope.
 Local Open Scope real_scope.
 
+HB.mixin Record Zmodule_isSubNormed (R : numDomainType)
+    (M : normedZmodType R) (S : pred M) T & SubChoice M S T
+    & Num.NormedZmodule R T := {
+  norm_valE : forall x , @Num.norm _ M ((val : T -> M) x) = @Num.norm _ T x
+}.
+
+(* couldn't be put in mathcomp_extra.v, error:
+
+Error:
+You must declare the hierarchy bottom-up or add a missing join.
+There are two ways out:
+- declare structure SubNormedZmodule before structure Num.SubNormedZmodule if Num.SubNormedZmodule inherits from it;
+- declare an additional structure that inherits from both Num.SemiNormedZmodule and SubType and from which SubNormedZmodule and/or Num.SubNormedZmodule inherit.
+
+*)
+#[short(type="subNormedZmodType")]
+HB.structure Definition SubNormedZmodule (R : numDomainType)
+    (V : normedZmodType R) (S : pred V) :=
+  { U of SubChoice V S U & Num.NormedZmodule R U & GRing.SubZmodule V S U
+    & Zmodule_isSubNormed R V S U }.
+
 HB.mixin Record isSubNbhs
   (V : nbhsType) (S : pred V) U & SubChoice V S U & Nbhs U := {
   continuous_valE : continuous (val : U -> V)