src/HOL/Real_Vector_Spaces.thy

--- a/src/HOL/Real_Vector_Spaces.thy	Mon Jan 30 10:15:01 2023 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon Jan 30 15:24:17 2023 +0000
@@ -159,6 +159,11 @@
     by simp
 qed
 
+lemma shift_zero_ident [simp]:
+  fixes f :: "'a \<Rightarrow> 'b::real_vector"
+  shows "(+)0 \<circ> f = f"
+  by force
+  
 lemma linear_scale_real:
   fixes r::real shows "linear f \<Longrightarrow> f (r * b) = r * f b"
   using linear_scale by fastforce