src/HOL/Rings.thy

--- a/src/HOL/Rings.thy	Tue Nov 26 08:09:44 2019 +0100
+++ b/src/HOL/Rings.thy	Tue Nov 26 14:32:08 2019 +0000
@@ -128,6 +128,11 @@
 
 end
 
+lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = (*) 0"
+  by auto
+
+lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = (*) 1"
+  by auto
 
 subsection \<open>Abstract divisibility\<close>