{α : Type u_1} →
  [inst : TopologicalSpace α] →
    {R : Type u_3} →
      {M : Type u_5} →
        [inst_1 : TopologicalSpace M] →
          [inst_2 : Monoid R] →
            [inst_3 : AddMonoid M] →
              [inst_4 : DistribMulAction R M] →
                [inst_5 : ContinuousAdd M] → [ContinuousConstSMul R M] → DistribMulAction R C(α, M)