In arithmetic geometry, Faltings' product theorem gives sufficient conditions for a subvariety of a product of projective spaces to be a product of varieties in the projective spaces. It was introduced by in his proof of Lang's conjecture that subvarieties of an abelian variety containing no translates of non-trivial abelian subvarieties have only finitely many rational points.
and gave explicit versions of Faltings' product theorem.