{M : Type u_1} →
  {α : Type u_3} →
    {E : Type u_4} →
      [inst : MeasurableSpace α] →
        [inst_1 : NormedAddCommGroup E] →
          {μ : MeasureTheory.Measure α} →
            {p : ENNReal} →
              [inst_2 : Monoid M] →
                [inst_3 : MulAction M α] →
                  [MeasureTheory.SMulInvariantMeasure M α μ] →
                    [MeasurableConstSMul M α] → DistribMulAction Mᵈᵐᵃ ↥(MeasureTheory.Lp E p μ)