distribHaarChar_eq_of_measure_smul_eq_mul

English

If μ(g•s) = r μ(s) for some r ∈ ℝ≥0, then Δ(g) = r.

Русский

Если для множества s выполнено μ(g•s) = r μ(s) для некоторого r ≥ 0, то Δ(g) = r.

LaTeX

$$$μ(g\\cdot S) = r \\cdot μ(S) \\Rightarrow Δ(g) = r.$$$

Lean4

theorem distribHaarChar_eq_of_measure_smul_eq_mul (hs₀ : μ s ≠ 0) (hs : μ s ≠ ∞) {r : ℝ≥0}
    (hμgs : μ (g • s) = r * μ s) : distribHaarChar A g = r :=
  by
  refine ENNReal.coe_injective ?_
  rw [distribHaarChar_eq_div hs₀ hs, hμgs, ENNReal.mul_div_cancel_right] <;> simp [*]

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