theorem Algebra.IsGeometricallyReduced.isReduced_tensorProduct {k : Type u_1} [Field k] {R : Type u_2} [CommRing R] [Algebra k R] [IsGeometricallyReduced k R] {S : Type u_3} [CommRing S] [Algebra k S] : IsReduced (TensorProduct k S R)

If R is geometrically reduced over k and S is any reduced k-algebra, then R ⊗[k] S is reduced.