The prime factorisation of the radical of a natural number

The radical UniqueFactorizationMonoid.radical n of a natural number n is the product of its distinct prime factors, so each prime factor of n occurs in it exactly once. This file records that factorisation, which turns divisibility statements involving a radical into inequalities between exponents of primes.

Main results

• Nat.factorization_radical_apply: the exponent of p in radical n is 1 when p is a prime factor of n, and 0 otherwise.

theorem Nat.factorization_radical_apply (n p : ℕ) : (UniqueFactorizationMonoid.radical n).factorization p = if p ∈ n.primeFactors then 1 else 0

Each prime factor of n occurs exactly once in its radical: the exponent of p in radical n is 1 when p is a prime factor of n, and 0 otherwise.