Lemmas about squarefreeness of natural numbers

A number is squarefree when it is not divisible by any squares except the squares of units.

Main Results

• Nat.squarefree_iff_nodup_primeFactorsList: A positive natural number x is squarefree iff the list factors x has no duplicate factors.

Tags

squarefree, multiplicity

theorem Nat.squarefree_iff_nodup_primeFactorsList {n : ℕ} (h0 : n ≠ 0) : Squarefree n ↔ n.primeFactorsList.Nodup

theorem Squarefree.nodup_primeFactorsList {n : ℕ} (hn : Squarefree n) : n.primeFactorsList.Nodup

theorem Nat.squarefree_iff_prime_squarefree {n : ℕ} : Squarefree n ↔ ∀ (x : ℕ), Prime x → ¬x * x ∣ n

theorem Squarefree.natFactorization_le_one {n : ℕ} (p : ℕ) (hn : Squarefree n) : n.factorization p ≤ 1

theorem Nat.factorization_eq_one_of_squarefree {n p : ℕ} (hn : Squarefree n) (hp : Prime p) (hpn : p ∣ n) : n.factorization p = 1

theorem Nat.squarefree_of_factorization_le_one {n : ℕ} (hn : n ≠ 0) (hn' : ∀ (p : ℕ), n.factorization p ≤ 1) : Squarefree n

theorem Nat.squarefree_iff_factorization_le_one {n : ℕ} (hn : n ≠ 0) : Squarefree n ↔ ∀ (p : ℕ), n.factorization p ≤ 1

theorem Nat.Squarefree.ext_iff {n m : ℕ} (hn : Squarefree n) (hm : Squarefree m) : n = m ↔ ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)

theorem Nat.squarefree_pow_iff {n k : ℕ} (hn : n ≠ 1) (hk : k ≠ 0) : Squarefree (n ^ k) ↔ Squarefree n ∧ k = 1

theorem Nat.squarefree_and_prime_pow_iff_prime {n : ℕ} : Squarefree n ∧ IsPrimePow n ↔ Prime n

@[irreducible]

def Nat.minSqFacAux : ℕ → ℕ → Option ℕ

Assuming that n has no factors less than k, returns the smallest prime p such that p^2 ∣ n.

Equations

• One or more equations did not get rendered due to their size.

def Nat.minSqFac (n : ℕ) : Option ℕ

Returns the smallest prime factor p of n such that p^2 ∣ n, or none if there is no such p (that is, n is squarefree). See also Nat.squarefree_iff_minSqFac.

Equations

• n.minSqFac = if 2 ∣ n then have n' := n / 2; if 2 ∣ n' then some 2 else n'.minSqFacAux 3 else n.minSqFacAux 3

def Nat.MinSqFacProp (n : ℕ) : Option ℕ → Prop

The correctness property of the return value of minSqFac.

• If none, then n is squarefree;
• If some d, then d is a minimal square factor of n

Equations

• n.MinSqFacProp none = Squarefree n
• n.MinSqFacProp (some d) = (Nat.Prime d ∧ d * d ∣ n ∧ ∀ (p : ℕ), Nat.Prime p → p * p ∣ n → d ≤ p)

theorem Nat.minSqFacProp_div (n : ℕ) {k : ℕ} (pk : Prime k) (dk : k ∣ n) (dkk : ¬k * k ∣ n) {o : Option ℕ} (H : (n / k).MinSqFacProp o) : n.MinSqFacProp o

theorem Nat.minSqFacAux_has_prop {n : ℕ} (k : ℕ) (n0 : 0 < n) (i : ℕ) (e : k = 2 * i + 3) (ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m) : n.MinSqFacProp (n.minSqFacAux k)

theorem Nat.minSqFac_has_prop (n : ℕ) : n.MinSqFacProp n.minSqFac

theorem Nat.minSqFac_prime {n d : ℕ} (h : n.minSqFac = some d) : Prime d

theorem Nat.minSqFac_dvd {n d : ℕ} (h : n.minSqFac = some d) : d * d ∣ n

theorem Nat.minSqFac_le_of_dvd {n d : ℕ} (h : n.minSqFac = some d) {m : ℕ} (m2 : 2 ≤ m) (md : m * m ∣ n) : d ≤ m

theorem Nat.squarefree_iff_minSqFac {n : ℕ} : Squarefree n ↔ n.minSqFac = none

@[instance_reducible]

instance Nat.instDecidablePredSquarefree : DecidablePred Squarefree

Equations

• x✝.instDecidablePredSquarefree = decidable_of_iff' (x✝.minSqFac = none) ⋯

theorem Nat.squarefree_two : Squarefree 2

theorem Nat.divisors_filter_squarefree_of_squarefree {n : ℕ} (hn : Squarefree n) : {d ∈ n.divisors | Squarefree d} = n.divisors

theorem Nat.divisors_filter_squarefree {n : ℕ} (h0 : n ≠ 0) : {d ∈ n.divisors | Squarefree d}.val = Multiset.map (fun (x : Finset ℕ) => x.val.prod) (UniqueFactorizationMonoid.normalizedFactors n).toFinset.powerset.val

theorem Nat.sum_divisors_filter_squarefree {n : ℕ} (h0 : n ≠ 0) {α : Type u_1} [AddCommMonoid α] {f : ℕ → α} : ∑ d ∈ n.divisors with Squarefree d, f d = ∑ i ∈ (UniqueFactorizationMonoid.normalizedFactors n).toFinset.powerset, f i.val.prod

@[deprecated "Use `exists_sq_mul_squarefree` instead, which binds the witnesses in the order in which they appear." (since := "2026-08-17")]

theorem Nat.sq_mul_squarefree (n : ℕ) : ∃ (a : ℕ) (b : ℕ), b ^ 2 * a = n ∧ Squarefree a

theorem Nat.sq_mul_squarefree_of_pos {n : ℕ} (hn : 0 < n) : ∃ (a : ℕ) (b : ℕ), 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

theorem Nat.sq_mul_squarefree_of_pos' {n : ℕ} (h : 0 < n) : ∃ (a : ℕ) (b : ℕ), (b + 1) ^ 2 * (a + 1) = n ∧ Squarefree (a + 1)

theorem Nat.squarefree_mul {m n : ℕ} (hmn : m.Coprime n) : Squarefree (m * n) ↔ Squarefree m ∧ Squarefree n

Squarefree is multiplicative. Note that the → direction does not require hmn and generalizes to arbitrary commutative monoids. See Squarefree.of_mul_left and Squarefree.of_mul_right above for auxiliary lemmas.

theorem Nat.coprime_of_squarefree_mul {m n : ℕ} (h : Squarefree (m * n)) : m.Coprime n

theorem Nat.squarefree_mul_iff {m n : ℕ} : Squarefree (m * n) ↔ m.Coprime n ∧ Squarefree m ∧ Squarefree n

theorem Nat.coprime_div_gcd_of_squarefree {m n : ℕ} (hm : Squarefree m) (hn : n ≠ 0) : (m / m.gcd n).Coprime n

theorem Nat.prod_primeFactors_of_squarefree {n : ℕ} (hn : Squarefree n) : ∏ p ∈ n.primeFactors, p = n

theorem Nat.squarefree_and_primeFactors_card_eq_two_iff (n : ℕ) : Squarefree n ∧ n.primeFactors.card = 2 ↔ ∃ (p : ℕ) (q : ℕ), p < q ∧ Prime p ∧ Prime q ∧ p * q = n

theorem Nat.primeFactors_prod {s : Finset ℕ} (hs : ∀ p ∈ s, Prime p) : (∏ p ∈ s, p).primeFactors = s

theorem Nat.primeFactors_prod_primeFactors (n : ℕ) : (∏ p ∈ n.primeFactors, p).primeFactors = n.primeFactors

theorem Nat.prod_primeFactors_dvd_iff {n k : ℕ} (hk : k ≠ 0) : ∏ p ∈ n.primeFactors, p ∣ k ↔ n.primeFactors ⊆ k.primeFactors

theorem Nat.primeFactors_div_gcd {m n : ℕ} (hm : Squarefree m) (hn : n ≠ 0) : (m / m.gcd n).primeFactors = m.primeFactors \ n.primeFactors

theorem Nat.prod_primeFactors_invOn_squarefree : Set.InvOn (fun (n : ℕ) => n.factorization.support) (fun (s : Finset ℕ) => ∏ p ∈ s, p) {s : Finset ℕ | ∀ p ∈ s, Prime p} {n : ℕ | Squarefree n}

theorem Nat.prod_primeFactors_sdiff_of_squarefree {n : ℕ} (hn : Squarefree n) {t : Finset ℕ} (ht : t ⊆ n.primeFactors) : ∏ a ∈ n.primeFactors \ t, a = n / ∏ a ∈ t, a

theorem Int.squarefree_iff_prime_sq_not_dvd {n : ℤ} : Squarefree n ↔ ∀ (p : ℕ), Nat.Prime p → ¬↑p ^ 2 ∣ n

An integer is squarefree iff no prime square divides it.