cleanup

IBM · Jan 24, 2025 · 55f411b · 55f411b
1 parent fe6d8e1
commit 55f411b
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 450 deletions.
diff --git a/coq/ProbTheory/RealVectorHilbert.v b/coq/ProbTheory/RealVectorHilbert.v
@@ -586,6 +586,14 @@ Section Rvector_defs.
     lra.
   Qed.
 
+  Lemma Rvector_mult_plus_distr_l (x y z : vector R n) :
+    x * (y + z) =  (x * y) + (x * z).
+  Proof.
+    rewrite Rvector_mult_comm.
+    rewrite Rvector_mult_plus_distr_r.
+    now repeat rewrite (Rvector_mult_comm x _).
+  Qed.
+
   Lemma Rvector_sum_plus_distr (x y:vector R n) :
     ∑ (x + y) = (∑ x + ∑ y)%R.
   Proof.