Formal target: Corpus.Erdos373.erdos_373

Show that the equation n!=a_1!a_2!···a_k!, with n−1 > a_1 ≥ a_2 ≥ ··· ≥ a_k, has only finitely many solutions.

Exact formal statement

Set.Finite.{0} Corpus.Erdos373.S

This target is a formal statement, not a proof of the problem.

Environment availability: available.