Theorems · Theorem · measure theory

MeasureTheory.integral_domSMul

∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {G : Type u_6} {A : Type u_7}
  [inst_2 : Group G] [inst_3 : AddCommGroup A] [inst_4 : DistribMulAction G A] [inst_5 : MeasurableSpace A]
  [inst_6 : MeasurableConstSMul G A] {μ : MeasureTheory.Measure A} (g : Gᵈᵐᵃ) (f : A → E),
  ∫ (x : A), f x ∂g • μ = ∫ (x : A), f ((DomMulAct.mk.symm g)⁻¹ • x) ∂μ

Defined in

Mathlib.MeasureTheory.Integral.Bochner.Basic

Cited by

1 results in Mathlib

Foundations

Depth 257 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceGroupAddCommGroupDistribMulActionMeasurableSpaceMeasurableConstSMul