rw [fderiv_fourierChar_apply]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ (fderiv ℝ (fun x => ↑(fourierChar (Multiplicative.ofAdd x))) x) dx =
    ((2 * ↑π * I * ↑(fourierChar (Multiplicative.ofAdd x))) • ofRealCLM) dx
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ (2 * π * dx) • (I * ↑(fourierChar (Multiplicative.ofAdd x))) =
    ((2 * ↑π * I * ↑(fourierChar (Multiplicative.ofAdd x))) • ofRealCLM) dx