∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [ContinuousNeg G] {X : Type u_2}
  [inst_3 : TopologicalSpace X] [R1Space X] [inst_5 : MeasurableSpace X] [BorelSpace X] [inst_7 : AddAction G X]
  [ContinuousVAdd G X] {g : G},
  (DenseRange fun x => x • g) →
    ∀ (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicVAdd G X μ],
      Ergodic (fun x => g +ᵥ x) μ