--- a/src/HOL/Analysis/Complex_Transcendental.thy Sun Jun 02 14:11:09 2024 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Mon Jun 03 20:56:21 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
--- a/src/HOL/Transcendental.thy Sun Jun 02 14:11:09 2024 +0200
+++ b/src/HOL/Transcendental.thy Mon Jun 03 20:56:21 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)