English
Let μ be an additive Haar measure on a suitable locally compact additive group E, and let L be a continuous linear equivalence E ≃SL[σ] F. Then the pushforward measure μ.map L is a Haar measure on F.
Русский
Пусть μ — мера Хаара на локально компактной аддитивной группе E, а L — непрерывное линейное эквивалентное отображение E ≃SL[σ] F. Тогда образующая мера μ.map L является мерой Хаара на F.
LaTeX
$$$IsAddHaarMeasure(\\mu.map L)$$$
Lean4
/-- A convenience wrapper for MeasureTheory.Measure.isAddHaarMeasure_map`. -/
instance _root_.ContinuousLinearEquiv.isAddHaarMeasure_map {E F R S : Type*} [Semiring R] [Semiring S] [AddCommGroup E]
[Module R E] [AddCommGroup F] [Module S F] [TopologicalSpace E] [IsTopologicalAddGroup E] [TopologicalSpace F]
[IsTopologicalAddGroup F] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ]
[MeasurableSpace E] [BorelSpace E] [MeasurableSpace F] [BorelSpace F] (L : E ≃SL[σ] F) (μ : Measure E)
[IsAddHaarMeasure μ] : IsAddHaarMeasure (μ.map L) :=
AddEquiv.isAddHaarMeasure_map _ (L : E ≃+ F) L.continuous L.symm.continuous
