∀ {G₀ : Type u_3} {β : Type u_5} {α : Type u_6} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace α] {f : α → β}
  [inst_2 : GroupWithZero G₀] [inst_3 : MulAction G₀ β] [MeasurableConstSMul G₀ β] {c : G₀},
  c ≠ 0 → ((Measurable fun x => c • f x) ↔ Measurable f)