Add am_lm_equiv_ms,

    fct_lm_gather_ms, am_gather{_equiv,,_rev}_ms (proofs redone, why?)

Algebra/AffineSpace/AffineSpace_aff_map.v

@@ -689,6 +689,10 @@ Lemma am_normal_rev_ms :
       sum L = 1 -> f (barycenter_ms L A1) = barycenter_ms L (mapF f A1).
 Proof. intro; apply am_normal_rev. Qed.
 
+Lemma am_lm_equiv_ms :
+  forall {f : E1 -> E2} O1, aff_map_ms f <-> lin_map (fct_lm_ms f O1).
+Proof. intro; apply am_lm_equiv. Qed.
+
 Lemma lm_am : forall {f : E1 -> E2}, lin_map f -> aff_map_ms f.
 Proof.
 intros; apply am_lm_0; apply lm_fct_minus;
@@ -708,19 +712,31 @@ Lemma am_comp_ms :
     aff_map_ms f12 -> aff_map_ms f23 -> aff_map_ms (f23 \o f12).
 Proof. move=>>; apply am_comp. Qed.
 
-Lemma am_gather_rev_ms :
+(* FIXME: COMMENTS TO BE REMOVED FOR PUBLICATION!
+  TODO FC (07/03/2025): understand why we have to redo the following proofs. *)
+Lemma fct_lm_gather_ms :
+  forall {n} (f : '(E1 -> E2)^n) O1,
+    fct_lm_ms (gather f) O1 = gather (fun i => fct_lm_ms (f i) O1).
+Proof. easy. Qed.
+
+Lemma am_gather_equiv_ms :
   forall {n} (f : '(E1 -> E2)^n),
-    aff_map_ms (gather f) -> forall i, aff_map_ms (f i).
+    aff_map_ms (gather f) <-> (forall i, aff_map_ms (f i)).
 Proof.
-move=>> Hf; apply am_gather_rev =>> HL; extF i; rewrite Hf//.
-move: i; apply extF_rev.
-
-
-
-
+intros n f; pose (O1 := point_of_as E1).
+rewrite (am_lm_equiv_ms O1) fct_lm_gather_ms lm_gather_equiv.
+apply equiv_forall; intro; rewrite am_lm_equiv_ms; easy.
+Qed.
 
+Lemma am_gather_ms :
+  forall {n} (f : '(E1 -> E2)^n),
+    (forall i, aff_map_ms (f i)) -> aff_map_ms (gather f).
+Proof. move=>>; apply am_gather_equiv_ms. Qed.
 
-Admitted.
+Lemma am_gather_rev_ms :
+  forall {n} (f : '(E1 -> E2)^n),
+    aff_map_ms (gather f) -> forall i, aff_map_ms (f i).
+Proof. move=>>; apply am_gather_equiv_ms. Qed.
 
 End ModuleSpace_AffineSpace_Morphism_Facts2.