(R₁ : Type u_1) →
  [inst : Semiring R₁] →
    {M₁ : Type u_4} →
      [inst_1 : TopologicalSpace M₁] →
        [inst_2 : AddCommMonoid M₁] →
          [inst_3 : Module R₁ M₁] → [inst_4 : TopologicalSpace R₁] → [ContinuousSMul R₁ M₁] → M₁ → R₁ →L[R₁] M₁