ring
case h.e'_3
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
this : ∫ (t : ℝ) in Ioi 0, 1 * hh (1 / (2 * π)) (t / 1) = 1 * 1 / (1 / (2 * π)) * π
⊢ 2 * π ^ 2 = 2 * π * π
no goals