{M : Type u_1} →
  [inst : SeminormedAddCommGroup M] →
    {R : Type u_3} →
      [inst_1 : Ring R] →
        [inst_2 : Module R M] →
          (S : Submodule R M) →
            (𝕜 : Type u_4) →
              [inst_3 : NormedField 𝕜] →
                [inst_4 : NormedSpace 𝕜 M] → [inst_5 : SMul 𝕜 R] → [IsScalarTower 𝕜 R M] → NormedSpace 𝕜 (M ⧸ S)