Tensor product of field extensions is nonzero (source code)

= Tensor product of field extensions is nonzero
{title2=$L\otimes_KL^{\prime}\ne0$}

If $L,L^{\prime}$ are <field extensions> of $K$, choose a $K$-basis of $L$ containing $1$. After tensoring with $L^{\prime}$, that basis expresses $L\otimes_KL^{\prime}$ as a nonzero direct sum of copies of $L^{\prime}$, and $1\otimes1$ is nonzero. A <prime ideal> of this nonzero ring supplies a point used in the <point-lifting property of a scheme fibre product>.