diag

Open

HlawkaGaussian.dbg_inner3

by sorry_not_sorry · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

diag

diagnostic

Preamble

import Mathlib
open MeasureTheory ProbabilityTheory

Formal statement

theorem HlawkaGaussian.dbg_inner3 : ∀ {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v w : E), inner (𝕜 := ℝ) v w = inner (𝕜 := ℝ) w v := by sorry

Source

diag

View graph