# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1513009712 -3600
# Node ID a77d54ef718b905696f291dd36a7e902903bae17
# Parent  22a5822f52f7278698d2ae1d8cb21aaa926b8aa8
Some facts on the Mangoldt function

diff -r 22a5822f52f7 -r a77d54ef718b src/HOL/Number_Theory/Prime_Powers.thy
--- 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] .