`BookProof.ChapterGaugeCasimirAverage.gaugeAverage_const` (μ : Measure G) [IsProbabilityMeasure μ] (c : ℝ) : gaugeAverage (X := X) μ (fun _ => c) = fun _ => c

Initializing...

`BookProof.ChapterGaugeCasimirAverage.gaugeAverage_const` (μ : Measure G) [IsProbabilityMeasure μ] (c : ℝ) : gaugeAverage (X := X) μ (fun _ => c) = fun _ => c · Prove2Me