addHaarScalarFactor_smul_congr' — Mathlib

English

For any g in G, the equality of scalar factors after applying g-scalar to μ and ν holds.

Русский

Для любого g в G равенство коэффициентов после применения g-скаляра к μ и ν; сохраняется.

LaTeX

$$$\\forall G \\; [Group G] \\; [A \\text{AddGroup}] \\; [DistribMulAction G A] \\; (μ : \\mathrm{Measure}(A)) \\; {ν : \\mathrm{Measure}(A)} \\, (g : G) \\, \\, addHaarScalarFactor (g \\cdot μ) (g \\cdot ν) = 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]

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