Theorem: fourierCoeffOn_sub (Carleson/Theorem1_1/Basic.lean)

State before:
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ fourierCoeffOn hab (f - g) n = fourierCoeffOn hab f n - fourierCoeffOn hab g n
Tactic:
rw [sub_eq_add_neg, fourierCoeffOn_add hf hg.neg, fourierCoeffOn_neg, ← sub_eq_add_neg]
State after:
no goals