∀ {α : Type u_1} {β : Type u_2} {f : α → β} {M : Type u_5} [inst : TopologicalSpace β] [inst_1 : Monoid M]
  [inst_2 : MulAction M β] [ContinuousConstSMul M β] {x : MeasurableSpace α} {c : M},
  IsUnit c → ((MeasureTheory.StronglyMeasurable fun x => c • f x) ↔ MeasureTheory.StronglyMeasurable f)