addHaarScalarFactor_smul_congr — Mathlib

English

The scalar factor does not change when the measures are uniformly rescaled by the same group action.

Русский

Масштабирование обеих мер одинаковым образом не изменяет коэффициент скаляра.

LaTeX

$$$\\forall G \\; [Group G] \\; [A \\,\\text{AddGroup}] \\, [DistribMulAction G A] \\, (μ, ν : \\mathrm{Measure}(A)) \\, (g : G) \\, (μ' := g \\cdot μ) \\, (ν' := g \\cdot ν) \\\\text{then } addHaarScalarFactor μ' ν' = addHaarScalarFactor μ ν$$

Lean4

theorem addHaarScalarFactor_smul_congr (g : Gᵈᵐᵃ) : addHaarScalarFactor μ (g • μ) = addHaarScalarFactor ν (g • ν) := by
  rw [addHaarScalarFactor_eq_mul _ (g • ν), addHaarScalarFactor_domSMul, mul_comm, ← addHaarScalarFactor_eq_mul]

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