# mathlib3documentation

data.nat.squarefree

# Lemmas about squarefreeness of natural numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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) :
theorem nat.squarefree_of_factorization_le_one {n : } (hn : n 0) (hn' : (p : ), (n.factorization) p 1) :
theorem nat.squarefree_iff_factorization_le_one {n : } (hn : n 0) :
(p : ), (n.factorization) p 1
theorem nat.squarefree.ext_iff {n m : } (hn : squarefree n) (hm : squarefree m) :
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

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

Equations
def nat.min_sq_fac (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 squarefree_iff_min_sq_fac.

Equations
def nat.min_sq_fac_prop (n : ) :
Prop

The correctness property of the return value of min_sq_fac.

• If none, then n is squarefree;
• If some d, then d is a minimal square factor of n
Equations
theorem nat.min_sq_fac_prop_div (n : ) {k : } (pk : nat.prime k) (dk : k n) (dkk : ¬k * k n) {o : option } (H : (n / k).min_sq_fac_prop o) :
theorem nat.min_sq_fac_aux_has_prop {n : } (k : ) :
0 < n (i : ), k = 2 * i + 3 ( (m : ), m n k m) n.min_sq_fac_prop (n.min_sq_fac_aux k)
theorem nat.min_sq_fac_prime {n d : } (h : n.min_sq_fac = ) :
theorem nat.min_sq_fac_dvd {n d : } (h : n.min_sq_fac = ) :
d * d n
theorem nat.min_sq_fac_le_of_dvd {n d : } (h : n.min_sq_fac = ) {m : } (m2 : 2 m) (md : m * m n) :
d m
@[protected, instance]
Equations
theorem nat.divisors_filter_squarefree {n : } (h0 : n 0) :
= multiset.map (λ (x : , x.val.prod)
theorem nat.sum_divisors_filter_squarefree {n : } (h0 : n 0) {α : Type u_1} {f : α} :
(λ (i : ), f i) = (λ (i : , f i.val.prod)
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 : m.coprime 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.

### Square-free prover #

A predicate representing partial progress in a proof of squarefree.

Equations
theorem tactic.norm_num.squarefree_helper_0 {k : } (k0 : 0 < k) {p : } (pp : nat.prime p) (h : bit1 k p) :
bit1 (k + 1) p bit1 k = p
theorem tactic.norm_num.squarefree_helper_1 (n k k' : ) (e : k + 1 = k') (hk : nat.prime (bit1 k) ¬bit1 k bit1 n) (H : k') :
theorem tactic.norm_num.squarefree_helper_2 (n k k' c : ) (e : k + 1 = k') (hc : bit1 n % bit1 k = c) (c0 : 0 < c) (h : k') :
theorem tactic.norm_num.squarefree_helper_3 (n n' k k' c : ) (e : k + 1 = k') (hn' : bit1 n' * bit1 k = bit1 n) (hc : bit1 n' % bit1 k = c) (c0 : 0 < c) (H : k') :
theorem tactic.norm_num.squarefree_helper_4 (n k k' : ) (e : bit1 k * bit1 k = k') (hd : bit1 n < k') :
theorem tactic.norm_num.not_squarefree_mul (a aa b n : ) (ha : a * a = aa) (hb : aa * b = n) (h₁ : 1 < a) :
meta def tactic.norm_num.prove_non_squarefree (e : expr) (n a : ) :

Given e a natural numeral and a : nat with a^2 ∣ n, return ⊢ ¬ squarefree e.

meta def tactic.norm_num.prove_squarefree_aux (ic : tactic.instance_cache) (en en1 : expr) (n1 : ) (ek : expr) (k : ) :

Given en,en1 := bit1 en, n1 the value of en1, ek, returns ⊢ squarefree_helper en ek.

meta def tactic.norm_num.prove_squarefree (en : expr) (n : ) :

Given n > 0 a squarefree natural numeral, returns ⊢ squarefree n.

Evaluates the squarefree predicate on naturals.