instIsHaarMeasure — Mathlib

English

If μ and ν are Haar measures on groups G and H, then the product measure μ × ν is a Haar measure on the product group G × H.

Русский

Если μ и ν — меры Хаара на группах G и H, то произведение μ × ν является мерой Хаара на произведении групп G × H.

LaTeX

$$IsHaarMeasure(μ × ν)$$

Lean4

@[to_additive]
instance instIsHaarMeasure {G : Type*} [Group G] [TopologicalSpace G] {_ : MeasurableSpace G} {H : Type*} [Group H]
    [TopologicalSpace H] {_ : MeasurableSpace H} (μ : Measure G) (ν : Measure H) [IsHaarMeasure μ] [IsHaarMeasure ν]
    [SFinite μ] [SFinite ν] [MeasurableMul G] [MeasurableMul H] : IsHaarMeasure (μ.prod ν) where

Похожие утверждения