∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedRing 𝕜] [inst_2 : Module 𝕜 E] [inst_3 : IsBoundedSMul 𝕜 E]
  [inst_4 : Fact (1 ≤ p)], IsBoundedSMul 𝕜 ↥(MeasureTheory.Lp E p μ)