Theorem: Continuous.realFourierChar (ForML/Trigonometric.lean)

State before:
E : Type u_1
inst✝ : TopologicalSpace E
f : E → ℝ
hf : Continuous f
⊢ Continuous fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (f x)))
Tactic:
simp_rw [Real.fourierChar_apply]
State after:
E : Type u_1
inst✝ : TopologicalSpace E
f : E → ℝ
hf : Continuous f
⊢ Continuous fun x => cexp (↑(2 * π * f x) * I)

State before:
E : Type u_1
inst✝ : TopologicalSpace E
f : E → ℝ
hf : Continuous f
⊢ Continuous fun x => cexp (↑(2 * π * f x) * I)
Tactic:
simp_rw [← Complex.real_smul]
State after:
E : Type u_1
inst✝ : TopologicalSpace E
f : E → ℝ
hf : Continuous f
⊢ Continuous fun x => cexp ((2 * π * f x) • I)

State before:
E : Type u_1
inst✝ : TopologicalSpace E
f : E → ℝ
hf : Continuous f
⊢ Continuous fun x => cexp ((2 * π * f x) • I)
Tactic:
exact ((continuous_const.mul hf).smul continuous_const).cexp
State after:
no goals