Theorem: gg_of_hh (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : x ≠ 0
i : ℝ
⊢ gg x i = x⁻¹ * hh (1 / (2 * π)) (i / x)
Tactic:
field_simp [gg, hh]
State after:
no goals