∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Add G] [MeasurableAdd G] (μ : MeasureTheory.Measure G),
  (∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h => h + g) ⁻¹' A) = μ A) ↔ μ.IsAddRightInvariant