∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : LocallyCompactSpace G] (g : G),
  MeasureTheory.Measure.addModularCharacterFun g =
    (MeasureTheory.Measure.map (fun x => x + g) MeasureTheory.Measure.addHaar).addHaarScalarFactor
      MeasureTheory.Measure.addHaar