Nontriviality of tensor product of algebras

This file contains some more results on nontriviality of tensor product of algebras.

theorem Algebra.TensorProduct.nontrivial_of_algebraMap_injective_of_isDomain (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (ha : Function.Injective ⇑(algebraMap R A)) (hb : Function.Injective ⇑(algebraMap R B)) [IsDomain A] [IsDomain B] : Nontrivial (TensorProduct R A B)

If A, B are R-algebras, R injects into A and B, and A and B are domains (which implies R is also a domain), then A ⊗[R] B is nontrivial.