Removing prime-power factors

The least prime belongs to the prime factors of a natural number greater than one, and removing its full multiplicity gives a smaller number. Removing the p-part erases p from the prime factors. These facts support induction by successively removing prime-power blocks.

theorem Nat.minFac_mem_primeFactors {n : ℕ} (hn : 1 < n) : n.minFac ∈ n.primeFactors

For 1 < n the least prime factor of n is one of its primes.

theorem Nat.ordCompl_minFac_lt {n : ℕ} (hn : 1 < n) : n / n.minFac ^ n.factorization n.minFac < n

Peeling the block at the least prime factor makes n strictly smaller.

@[simp]

theorem Nat.primeFactors_ordCompl (n p : ℕ) : (n / p ^ n.factorization p).primeFactors = n.primeFactors.erase p

Removing the p-part of a natural number removes p from its prime factors.