chore(*complex*): add a few simp lemmas (#10187)

Author: urkud

src/analysis/special_functions/trigonometric/basic.lean

@@ -1059,16 +1059,22 @@ by simpa only [mul_inv_cancel_right₀ I_ne_zero] using exp_antiperiodic.mul_con
 lemma exp_mul_I_periodic : function.periodic (λ x, exp (x * I)) (2 * π) :=
 exp_mul_I_antiperiodic.periodic
 
-lemma exp_pi_mul_I : exp (π * I) = -1 :=
+@[simp] lemma exp_pi_mul_I : exp (π * I) = -1 :=
 exp_zero ▸ exp_antiperiodic.eq
 
-lemma exp_two_pi_mul_I : exp (2 * π * I) = 1 :=
+@[simp] lemma exp_two_pi_mul_I : exp (2 * π * I) = 1 :=
 exp_periodic.eq.trans exp_zero
 
-lemma exp_nat_mul_two_pi_mul_I (n : ℕ) : exp (n * (2 * π * I)) = 1 :=
+@[simp] lemma exp_nat_mul_two_pi_mul_I (n : ℕ) : exp (n * (2 * π * I)) = 1 :=
 (exp_periodic.nat_mul_eq n).trans exp_zero
 
-lemma exp_int_mul_two_pi_mul_I (n : ℤ) : exp (n * (2 * π * I)) = 1 :=
+@[simp] lemma exp_int_mul_two_pi_mul_I (n : ℤ) : exp (n * (2 * π * I)) = 1 :=
 (exp_periodic.int_mul_eq n).trans exp_zero
 
+@[simp] lemma exp_add_pi_mul_I (z : ℂ) : exp (z + π * I) = -exp z :=
+exp_antiperiodic z
+
+@[simp] lemma exp_sub_pi_mul_I (z : ℂ) : exp (z - π * I) = -exp z :=
+exp_antiperiodic.sub_eq z
+
 end complex

src/data/complex/basic.lean

@@ -234,6 +234,8 @@ lemma norm_sq_apply (z : ℂ) : norm_sq z = z.re * z.re + z.im * z.im := rfl
 @[simp] lemma norm_sq_of_real (r : ℝ) : norm_sq r = r * r :=
 by simp [norm_sq]
 
+@[simp] lemma norm_sq_mk (x y : ℝ) : norm_sq ⟨x, y⟩ = x * x + y * y := rfl
+
 lemma norm_sq_eq_conj_mul_self {z : ℂ} : (norm_sq z : ℂ) = conj z * z :=
 by { ext; simp [norm_sq, mul_comm], }
 

src/data/complex/exponential.lean

@@ -879,6 +879,12 @@ by { rw [exp_eq_exp_re_mul_sin_add_cos], simp [exp_of_real_re, cos_of_real_re] }
 lemma exp_im : (exp x).im = real.exp x.re * real.sin x.im :=
 by { rw [exp_eq_exp_re_mul_sin_add_cos], simp [exp_of_real_re, sin_of_real_re] }
 
+@[simp] lemma exp_of_real_mul_I_re (x : ℝ) : (exp (x * I)).re = real.cos x :=
+by simp [exp_mul_I, cos_of_real_re]
+
+@[simp] lemma exp_of_real_mul_I_im (x : ℝ) : (exp (x * I)).im = real.sin x :=
+by simp [exp_mul_I, sin_of_real_re]
+
 /-- **De Moivre's formula** -/
 theorem cos_add_sin_mul_I_pow (n : ℕ) (z : ℂ) :
   (cos z + sin z * I) ^ n = cos (↑n * z) + sin (↑n * z) * I :=