diag
ProvedHlawkaGaussian.dbg_intdiag
diagnostic
Preamble
import Mathlib open MeasureTheory ProbabilityTheory
Formal statement
theorem HlawkaGaussian.dbg_int : ∫ (t : ℝ), t ∂(ProbabilityTheory.gaussianReal 0 1) = 0 := by sorry
Source
diag
HlawkaGaussian.dbg_intdiagnostic
import Mathlib open MeasureTheory ProbabilityTheory
theorem HlawkaGaussian.dbg_int : ∫ (t : ℝ), t ∂(ProbabilityTheory.gaussianReal 0 1) = 0 := by sorry