A number below the square of its least prime factor

A candidate for Mathlib.Data.Nat.Prime.Defs, next to Nat.minFac_sq_le_self: a number other than 0 and 1 below p ^ 2 whose prime factors are all at least p is a prime.

Main statements

• Nat.prime_of_lt_mul_self: a number n ∉ {0, 1} below p ^ 2 with no prime factor below p is a prime.

theorem Nat.prime_of_lt_mul_self {n p : ℕ} (hn0 : n ≠ 0) (hn1 : n ≠ 1) (hlt : n < p * p) (h : ∀ (q : ℕ), Prime q → q ∣ n → p ≤ q) : Prime n

A number n ∉ {0, 1} below p ^ 2 whose prime factors are all at least p is a prime: a composite n has minFac n ^ 2 ≤ n (Nat.minFac_sq_le_self).