Prime divisibility of factorials

Main results

• Nat.Prime.not_sq_dvd_factorial: a prime occurs only once in its own factorial.

Since p! is the order of the permutation group on p points, this bound also shows that p ^ 2 cannot divide the order of any of its subgroups. This supplies the divisibility bound used in the Sylow step of Jordan's theorem.

theorem Nat.Prime.not_sq_dvd_factorial {p : ℕ} (hp : Prime p) : ¬p ^ 2 ∣ p.factorial

A prime occurs only once in its own factorial.