∀ {M : Type v} {α : Type w} [inst : VAdd M α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [MeasureTheory.VAddInvariantMeasure M α μ] (c : NNReal), MeasureTheory.VAddInvariantMeasure M α (c • μ)