measurePreserving_zpow — Mathlib

English

Let μ, μ′ be Haar measures. The z-powers of the map preserve measure in a compatible way.

Русский

Пусть μ и μ′ — меры Хаара. Применение степеней z к отображению сохраняет меру совместимо.

LaTeX

$$$\\forall G \\; [\\text{CommGroup } G] \\; [CompactSpace G] \\; [RootableBy G \\mathbb{Z}] \\; {n : \\mathbb{Z}}, n \\neq 0 \\\\Rightarrow \\text{measurePreserving } (g \\mapsto g^n) \\ μ \\ μ$$

Lean4

@[to_additive]
theorem measurePreserving_zpow [CompactSpace G] [RootableBy G ℤ] {n : ℤ} (hn : n ≠ 0) :
    MeasurePreserving (fun g : G => g ^ n) μ μ :=
  (zpowGroupHom n).measurePreserving (μ := μ) (continuous_zpow n) (RootableBy.surjective_pow G ℤ hn) rfl

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