--- a/src/HOL/Number_Theory/Prime_Powers.thy Fri Dec 08 19:25:47 2017 +0000
+++ b/src/HOL/Number_Theory/Prime_Powers.thy Mon Dec 11 17:28:32 2017 +0100
@@ -422,7 +422,13 @@
definition mangoldt :: "nat \<Rightarrow> 'a :: real_algebra_1" where
"mangoldt n = (if primepow n then of_real (ln (real (aprimedivisor n))) else 0)"
-
+
+lemma mangoldt_0 [simp]: "mangoldt 0 = 0"
+ by (simp add: mangoldt_def)
+
+lemma mangoldt_Suc_0 [simp]: "mangoldt (Suc 0) = 0"
+ by (simp add: mangoldt_def)
+
lemma of_real_mangoldt [simp]: "of_real (mangoldt n) = mangoldt n"
by (simp add: mangoldt_def)
@@ -481,6 +487,10 @@
with True show ?thesis by (auto simp: mangoldt_def abs_if)
qed (auto simp: mangoldt_def)
+lemma Re_mangoldt [simp]: "Re (mangoldt n) = mangoldt n"
+ and Im_mangoldt [simp]: "Im (mangoldt n) = 0"
+ by (simp_all add: mangoldt_def)
+
lemma abs_mangoldt [simp]: "abs (mangoldt n :: real) = mangoldt n"
using norm_mangoldt[of n, where ?'a = real, unfolded real_norm_def] .