`BookProof.ChapterSphericalPlancherel.integral_eq_two_mul_of_even_real` (h : ℝ → ℝ) (he : ∀ x, h (-x) = h x) : ∫ x : ℝ, h x = 2 * ∫ x in Ioi (0 : ℝ), h x

Initializing...

`BookProof.ChapterSphericalPlancherel.integral_eq_two_mul_of_even_real` (h : ℝ → ℝ) (he : ∀ x, h (-x) = h x) : ∫ x : ℝ, h x = 2 * ∫ x in Ioi (0 : ℝ), h x · Prove2Me