English
Haar is a canonical choice of a left-invariant measure on a locally compact group.
Русский
Хаар — канонический выбор лево-инвариантной меры на локально компактной группе.
LaTeX
$$haar[K0] = Haar measure on G$$
Lean4
/-- Let `μ` be a σ-finite left invariant measure on `G`. Then `μ` is equal to the Haar measure
defined by `K₀` iff `μ K₀ = 1`. -/
@[to_additive]
theorem haarMeasure_eq_iff (K₀ : PositiveCompacts G) (μ : Measure G) [SigmaFinite μ] [IsMulLeftInvariant μ] :
haarMeasure K₀ = μ ↔ μ K₀ = 1 :=
⟨fun h => h.symm ▸ haarMeasure_self, fun h => by rw [haarMeasure_unique μ K₀, h, one_smul]⟩