Theorem: dirichletKernel'_eq_zero (Carleson/Theorem1_1/Dirichlet_kernel.lean)

State before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) = 1
⊢ dirichletKernel' N x = 0
Tactic:
rw [dirichletKernel', neg_mul, exp_neg, h]
State after:
N : ℕ
x : ℝ
h : cexp (I * ↑x) = 1
⊢ cexp (I * ↑N * ↑x) / (1 - 1⁻¹) + cexp (-I * ↑N * ↑x) / (1 - 1) = 0

State before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) = 1
⊢ cexp (I * ↑N * ↑x) / (1 - 1⁻¹) + cexp (-I * ↑N * ↑x) / (1 - 1) = 0
Tactic:
simp
State after:
no goals