# 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 Squarefree.nodup_factors {n : } (hn : ) :
theorem Nat.squarefree_iff_prime_squarefree {n : } :
∀ (x : ), ¬x * x n
theorem Squarefree.natFactorization_le_one {n : } (p : ) (hn : ) :
p 1
theorem Nat.factorization_eq_one_of_squarefree {n : } {p : } (hn : ) (hp : ) (hpn : p n) :
p = 1
theorem Nat.squarefree_of_factorization_le_one {n : } (hn : n 0) (hn' : ∀ (p : ), p 1) :
theorem Nat.squarefree_iff_factorization_le_one {n : } (hn : n 0) :
∀ (p : ), p 1
theorem Nat.Squarefree.ext_iff {n : } {m : } (hn : ) (hm : ) :
n = m ∀ (p : ), (p n p m)
theorem Nat.squarefree_pow_iff {n : } {k : } (hn : n 1) (hk : k 0) :
Squarefree (n ^ k) k = 1
def Nat.minSqFacAux :

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.
Instances For
def Nat.minSqFac (n : ) :

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
• = if 2 n then let n' := n / 2; if 2 n' then some 2 else else
Instances For
def Nat.MinSqFacProp (n : ) :

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
Instances For
theorem Nat.minSqFacProp_div (n : ) {k : } (pk : ) (dk : k n) (dkk : ¬k * k n) {o : } (H : Nat.MinSqFacProp (n / k) o) :
theorem Nat.minSqFacAux_has_prop {n : } (k : ) (n0 : 0 < n) (i : ) (e : k = 2 * i + 3) (ih : ∀ (m : ), m nk m) :
theorem Nat.minSqFac_prime {n : } {d : } (h : ) :
theorem Nat.minSqFac_dvd {n : } {d : } (h : ) :
d * d n
theorem Nat.minSqFac_le_of_dvd {n : } {d : } (h : ) {m : } (m2 : 2 m) (md : m * m n) :
d m
theorem Nat.divisors_filter_squarefree {n : } (h0 : n 0) :
(Finset.filter Squarefree ()).val = Multiset.map (fun (x : ) => Multiset.prod x.val)
theorem Nat.sum_divisors_filter_squarefree {n : } (h0 : n 0) {α : Type u_1} [] {f : α} :
(Finset.sum (Finset.filter Squarefree ()) fun (i : ) => f i) = Finset.sum 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
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
theorem Nat.squarefree_mul {m : } {n : } (hmn : ) :

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)) :
theorem Nat.squarefree_mul_iff {m : } {n : } :
theorem Nat.coprime_div_gcd_of_squarefree {m : } {n : } (hm : ) (hn : n 0) :
theorem Nat.prod_primeFactors_of_squarefree {n : } (hn : ) :
(Finset.prod n.primeFactors fun (p : ) => p) = n
theorem Nat.primeFactors_prod {s : } (hs : ps, ) :
(Finset.prod s fun (p : ) => p).primeFactors = s
theorem Nat.primeFactors_div_gcd {m : } {n : } (hm : ) (hn : n 0) :
(m / Nat.gcd m n).primeFactors = m.primeFactors \ n.primeFactors
theorem Nat.prod_primeFactors_invOn_squarefree :
Set.InvOn (fun (n : ) => .support) (fun (s : ) => Finset.prod s fun (p : ) => p) {s : | ps, } {n : | }
theorem Nat.prod_primeFactors_sdiff_of_squarefree {n : } (hn : ) {t : } (ht : t n.primeFactors) :
(Finset.prod (n.primeFactors \ t) fun (a : ) => a) = n / Finset.prod t fun (a : ) => a