∀ {α : Type u_1} (𝕜 : Type u_3) (E : Type u_2) {m : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
  [inst : NormedAddCommGroup E] [inst_1 : NormedRing 𝕜] [inst_2 : Module 𝕜 E] [inst_3 : IsBoundedSMul 𝕜 E] (c : 𝕜),
  ∀ f ∈ (MeasureTheory.Lp E p μ).carrier, c • f ∈ (MeasureTheory.Lp E p μ).carrier