∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing T] [inst_4 : Algebra R T],
  (algebraMap R T).SurjectiveOnStalks → Topology.IsEmbedding (PrimeSpectrum.tensorProductTo R S T)