∀ (M : Type u_1) (α : Type u_2) [inst : SMul M α] {x : MeasurableSpace α} (μ : MeasureTheory.Measure α),
  MeasureTheory.SMulInvariantMeasure M α μ ↔ ∀ (c : M) ⦃s : Set α⦄, MeasurableSet s → μ ((fun x => c • x) ⁻¹' s) = μ s