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_factors: A positive natural number x is squarefree iff the list factors x has no duplicate factors.

Tags

squarefree, multiplicity

theorem Nat.squarefree_iff_nodup_factors {n : ℕ} (h0 : n ≠ 0) : Squarefree n ↔ List.Nodup (Nat.factors n)

theorem Squarefree.nodup_factors {n : ℕ} (hn : Squarefree n) : List.Nodup (Nat.factors n)

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

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

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

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

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

theorem Nat.Squarefree.ext_iff {n : ℕ} {m : ℕ} (hn : Squarefree n) (hm : Squarefree m) : n = m ↔ ∀ (p : ℕ), Nat.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 ↔ Nat.Prime n

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

• Nat.minSqFac n = if 2 ∣ n then let n' := n / 2; if 2 ∣ n' then some 2 else Nat.minSqFacAux n' 3 else Nat.minSqFacAux n 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

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

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

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

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

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

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

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

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

instance Nat.instDecidablePredNatSquarefreeMonoid : DecidablePred Squarefree

Equations

• Nat.instDecidablePredNatSquarefreeMonoid x = decidable_of_iff' (Nat.minSqFac x = none) ⋯

theorem Nat.squarefree_two : Squarefree 2

theorem Nat.divisors_filter_squarefree_of_squarefree {n : ℕ} (hn : Squarefree n) : Finset.filter Squarefree (Nat.divisors n) = Nat.divisors n

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

theorem Nat.sum_divisors_filter_squarefree {n : ℕ} (h0 : n ≠ 0) {α : Type u_1} [AddCommMonoid α] {f : ℕ → α} : (Finset.sum (Finset.filter Squarefree (Nat.divisors n)) fun (i : ℕ) => f i) = Finset.sum (Finset.powerset (Multiset.toFinset (UniqueFactorizationMonoid.normalizedFactors n))) fun (i : Finset ℕ) => f (Multiset.prod i.val)

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.sq_mul_squarefree (n : ℕ) : ∃ (a : ℕ) (b : ℕ), b ^ 2 * a = n ∧ Squarefree a

theorem Nat.squarefree_mul {m : ℕ} {n : ℕ} (hmn : Nat.Coprime m 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)) : Nat.Coprime m n

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

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

theorem Nat.prod_primeFactors_of_squarefree {n : ℕ} (hn : Squarefree n) : (Finset.prod n.primeFactors fun (p : ℕ) => p) = n

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

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

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

theorem Nat.prod_primeFactors_sdiff_of_squarefree {n : ℕ} (hn : Squarefree n) {t : Finset ℕ} (ht : t ⊆ n.primeFactors) : (Finset.prod (n.primeFactors \ t) fun (a : ℕ) => a) = n / Finset.prod t fun (a : ℕ) => a