∀ (X : Type u_1) {M : Type u_4} {R : Type u_3} {S : Type u_2} [inst : Zero X] [inst_1 : CommSemiring M]
  [inst_2 : TopologicalSpace X] [inst_3 : TopologicalSpace R] [inst_4 : TopologicalSpace S] [inst_5 : CommSemiring R]
  [inst_6 : StarRing R] [inst_7 : IsTopologicalSemiring R] [inst_8 : CommSemiring S] [inst_9 : StarRing S]
  [inst_10 : IsTopologicalSemiring S] [inst_11 : Module M R] [inst_12 : Module M S] (φ : R →⋆ₙₐ[M] S)
  (hφ : Continuous ⇑φ), { toFun := ⇑φ, continuous_toFun := hφ, map_zero' := ⋯ }.comp 0 = 0