# HG changeset patch
# User paulson
# Date 1717444601 -3600
# Node ID 5cb9fd414e92c839454b26fcc1af49edb6ce5680
# Parent  534c5e4f07c0b7bc1d71c9594f70b66e1f07cfc8# Parent  92a66f1df06e3aedcd4307625aa2c05855096865
merged

diff -r 534c5e4f07c0 -r 5cb9fd414e92 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Mon Jun 03 20:28:25 2024 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Mon Jun 03 20:56:41 2024 +0100
@@ -63,6 +63,9 @@
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>The Exponential Function\<close>
 
+lemma exp_npi_numeral: "exp (\<i> * pi * Num.numeral n)  = (-1) ^ Num.numeral n"
+  by (metis exp_of_nat2_mult exp_pi_i' of_nat_numeral)
+
 lemma norm_exp_i_times [simp]: "norm (exp(\<i> * of_real y)) = 1"
   by simp
 
diff -r 534c5e4f07c0 -r 5cb9fd414e92 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Mon Jun 03 20:28:25 2024 +0200
+++ b/src/HOL/Transcendental.thy	Mon Jun 03 20:56:41 2024 +0100
@@ -3878,6 +3878,18 @@
   for n :: nat
   by (simp add: mult.commute [of pi])
 
+lemma sin_npi_numeral [simp]: "sin(Num.numeral n * pi) = 0"
+  by (metis of_nat_numeral sin_npi)
+
+lemma sin_npi2_numeral [simp]: "sin (pi * Num.numeral n) = 0"
+  by (metis of_nat_numeral sin_npi2)
+
+lemma cos_npi_numeral [simp]: "cos (Num.numeral n * pi) = (- 1) ^ Num.numeral n"
+  by (metis cos_npi of_nat_numeral)
+
+lemma cos_npi2_numeral [simp]: "cos (pi * Num.numeral n) = (- 1) ^ Num.numeral n"
+  by (metis cos_npi2 of_nat_numeral)
+
 lemma cos_two_pi [simp]: "cos (2 * pi) = 1"
   by (simp add: cos_double)