addHaarScalarFactor_smul_eq_distribHaarChar_inv

English

For Haar measure μ on A and g ∈ G, addHaarScalarFactor μ (inv g • μ) = Δ(g)⁻¹.

Русский

Для меры Хаара μ на A и элемента g ∈ G выполняется addHaarScalarFactor μ (g^{-1} • μ) = Δ(g)^{-1}.

LaTeX

$$$\\mathrm{addHaarScalarFactor} \\; μ \\; ((\\mathrm{DomMulAct.mk} \\, g)^{-1} \\cdot μ) = Δ(g)^{-1}.$$$

Lean4

theorem addHaarScalarFactor_smul_eq_distribHaarChar_inv (g : G) :
    addHaarScalarFactor μ (DomMulAct.mk g • μ) = (distribHaarChar A g)⁻¹ := by
  rw [← map_inv, ← addHaarScalarFactor_smul_inv_eq_distribHaarChar μ, DomMulAct.mk_inv, inv_inv]

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