Documentation

Mathlib.Data.Nat.Squarefree

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) :

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.

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

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

Instances For

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)

Instances For

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

@[irreducible]

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) :

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

@[implicit_reducible]

instance Nat.instDecidablePredSquarefree :

DecidablePred Squarefree

Equations

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

theorem Nat.squarefree_two :

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

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 : 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)) :

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.primeFactors_prod {s : Finset ℕ} (hs : ∀ p ∈ s, Prime p) :

(∏ p ∈ s, p).primeFactors = s

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