Skip to content
Snippets Groups Projects
Commit 85d4c522 authored by François Clément's avatar François Clément
Browse files

Yet unused: procrastinate!

parent aff6c920
No related branches found
No related tags found
No related merge requests found
......@@ -939,6 +939,8 @@ Proof. intros; rewrite baryc_ms_eq//; apply lc_r_kron_r. Qed.
End Euclidean_space_AffineSpace.
(* FIXME: COMMENTS TO BE REMOVED FOR PUBLICATION!
TODO FC (07/03/2025): do this proof.
Section ModuleSpace_AffineSpace_R_Facts.
Context {K : Ring}.
......@@ -946,10 +948,11 @@ Context {V : ModuleSpace K}.
Context {E : AffineSpace V}.
Lemma baryc_comm_l_R :
forall {n1 n2} M (L : 'K^{n1,n2}) (A2 : 'E^n2),
barycenter (barycenter_ms M L) A2 =
barycenter M (mapF (barycenter^~ A2) L).
forall {n1 n2} L1 (M : 'K^{n1,n2}) (A2 : 'E^n2),
barycenter (barycenter_ms L1 M) A2 =
barycenter L1 (mapF (barycenter^~ A2) M).
Proof.
Admitted.
Aglopted.
End ModuleSpace_AffineSpace_R_Facts.
*)
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment