Theorem: k_of_neg_eq_conj_k (Carleson/Theorem1_1/Hilbert_kernel.lean)

State before:
x : ℝ
⊢ k (-x) = (starRingEnd ℂ) (k x)
Tactic:
simp [k, Complex.conj_ofReal, ←Complex.exp_conj, Complex.conj_I, neg_mul]
State after:
no goals