Theorems · Theorem · Lie groups

MeasureTheory.isMulRightInvariant_map_smul

∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Semigroup G] [MeasurableMul G] {μ : MeasureTheory.Measure G}
  {α : Type u_3} [inst_3 : SMul α G] [SMulCommClass α Gᵐᵒᵖ G] [MeasurableConstSMul α G] [μ.IsMulRightInvariant] (a : α),
  (MeasureTheory.Measure.map (fun x => a • x) μ).IsMulRightInvariant

The image of a right invariant measure under a left action is right invariant, assuming that the action preserves multiplication.

Defined in

Mathlib.MeasureTheory.Group.Measure

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceSemigroupMeasurableMulSMulSMulCommClassMeasurableConstSMulMeasureTheory.Measure.IsMulRightInvariant