src/HOL/Analysis/Linear_Algebra.thy

--- a/src/HOL/Analysis/Linear_Algebra.thy	Tue Jun 03 12:22:58 2025 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Tue Jun 03 15:18:54 2025 +0200
@@ -426,6 +426,18 @@
 lemma in_span_Basis: "x \<in> span Basis"
   unfolding span_Basis ..
 
+lemma representation_euclidean_space:
+  "representation Basis x = (\<lambda>b. if b \<in> Basis then inner x b else 0)"
+proof (rule representation_eqI)
+  have "(\<Sum>b | (if b \<in> Basis then inner x b else 0) \<noteq> 0. (if b \<in> Basis then inner x b else 0) *\<^sub>R b) =
+          (\<Sum>b\<in>Basis. inner x b *\<^sub>R b)"
+    by (intro sum.mono_neutral_cong_left) auto
+  also have "\<dots> = x"
+    by (simp add: euclidean_representation)
+  finally show "(\<Sum>b | (if b \<in> Basis then inner x b else 0) \<noteq> 0.
+                  (if b \<in> Basis then inner x b else 0) *\<^sub>R b) = x" .
+qed (insert independent_Basis span_Basis, auto split: if_splits)
+
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Linearity and Bilinearity continued\<close>