addHaarScalarFactor_smul_inv_eq_distribHaarChar

English

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

Русский

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

LaTeX

$$$\\mathrm{addHaarScalarFactor} \\, \\mu ((\\mathrm{DomMulAct.mk} \\, g)^{-1} \\cdot \\mu) = \\Delta(g)^{-1}. $$$

Lean4

theorem addHaarScalarFactor_smul_inv_eq_distribHaarChar (g : G) :
    addHaarScalarFactor μ ((DomMulAct.mk g)⁻¹ • μ) = distribHaarChar A g :=
  by
  rw [← addHaarScalarFactor_domSMul _ _ (DomMulAct.mk g)]
  simp_rw [← mul_smul, mul_inv_cancel, one_smul]
  exact addHaarScalarFactor_smul_eq_distribHaarChar ..

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