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 Nat.Squarefree.factorization_le_one {n : ℕ} (p : ℕ) (hn : Squarefree 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) (_ : Squarefree x ↔ 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 => 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 => 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.prod_factors_toFinset_of_squarefree {n : ℕ} (hn : Squarefree n) : (Finset.prod (List.toFinset (Nat.factors n)) fun p => p) = n