distribHaarChar_mul — Mathlib

English

For g ∈ G and s ⊆ A, Δ(g) μ(s) = μ(g • s).

Русский

Для любого g ∈ G и множества s ⊆ A выполняется Δ(g) μ(s) = μ(g•s).

LaTeX

$$$\\Delta(g) \\cdot \\mu(S) = \\mu(g\\cdot S)\\quad \\text{для всех } S \\subseteq A.$$$

Lean4

theorem distribHaarChar_mul (g : G) (s : Set A) : distribHaarChar A g * μ s = μ (g • s) :=
  by
  have : (DomMulAct.mk g • μ) s = μ (g • s) := by simp [domSMul_apply]
  rw [eq_comm, ← nnreal_smul_coe_apply, ← addHaarScalarFactor_smul_eq_distribHaarChar μ, ← this, ← smul_apply, ←
    isAddLeftInvariant_eq_smul_of_regular]

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