mathlib3 documentation

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 #

Tags #

squarefree, multiplicity

source
theorem nat.squarefree_iff_nodup_factors {n : ℕ} (h0 : n ≠ 0) :
squarefree n ↔ n.factors.nodup
source
theorem nat.squarefree_iff_prime_squarefree {n : ℕ} :
squarefree n ↔ ∀ (x : ℕ), nat.prime x → ¬x * x ∣ n
source
theorem nat.squarefree.factorization_le_one {n : ℕ} (p : ℕ) (hn : squarefree n) :
⇑(n.factorization) p ≤ 1
source
theorem nat.squarefree_of_factorization_le_one {n : ℕ} (hn : n ≠ 0) (hn' : ∀ (p : ℕ), ⇑(n.factorization) p ≤ 1) :
squarefree n
source
theorem nat.squarefree_iff_factorization_le_one {n : ℕ} (hn : n ≠ 0) :
squarefree n ↔ ∀ (p : ℕ), ⇑(n.factorization) p ≤ 1
source
theorem nat.squarefree.ext_iff {n m : ℕ} (hn : squarefree n) (hm : squarefree m) :
n = m ↔ ∀ (p : ℕ), nat.prime p → (p ∣ n ↔ p ∣ m)
source
theorem nat.squarefree_pow_iff {n k : ℕ} (hn : n ≠ 1) (hk : k ≠ 0) :
squarefree (n ^ k) ↔ squarefree n ∧ k = 1
source
theorem nat.squarefree_and_prime_pow_iff_prime {n : ℕ} :
squarefree n ∧ is_prime_pow n ↔ nat.prime n
source
def nat.min_sq_fac_aux  :
ℕ → ℕ → option ℕ

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

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

Equations
source
def nat.min_sq_fac_prop (n : ℕ) :
option ℕ → 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
source
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) :
n.min_sq_fac_prop o
source
theorem nat.min_sq_fac_aux_has_prop {n : ℕ} (k : ℕ) :
0 < n → ∀ (i : ℕ), k = 2 * i + 3 → (∀ (m : ℕ), nat.prime m → m ∣ n → k ≤ m) → n.min_sq_fac_prop (n.min_sq_fac_aux k)
source
theorem nat.min_sq_fac_has_prop (n : ℕ) :
n.min_sq_fac_prop n.min_sq_fac
source
theorem nat.min_sq_fac_prime {n d : ℕ} (h : n.min_sq_fac = option.some d) :
nat.prime d
source
theorem nat.min_sq_fac_dvd {n d : ℕ} (h : n.min_sq_fac = option.some d) :
d * d ∣ n
source
theorem nat.min_sq_fac_le_of_dvd {n d : ℕ} (h : n.min_sq_fac = option.some d) {m : ℕ} (m2 : 2 ≤ m) (md : m * m ∣ n) :
d ≤ m
source
theorem nat.squarefree_iff_min_sq_fac {n : ℕ} :
squarefree n ↔ n.min_sq_fac = option.none
source
@[protected, instance]
def nat.squarefree.decidable_pred  :
decidable_pred squarefree
Equations
source
theorem nat.squarefree_two  :
squarefree 2
source
theorem nat.divisors_filter_squarefree {n : ℕ} (h0 : n ≠ 0) :
(finset.filter squarefree n.divisors).val = multiset.map (λ (x : finset ℕ), x.val.prod) (unique_factorization_monoid.normalized_factors n).to_finset.powerset.val
source
theorem nat.sum_divisors_filter_squarefree {n : ℕ} (h0 : n ≠ 0) {α : Type u_1} [add_comm_monoid α] {f : ℕ → α} :
(finset.filter squarefree n.divisors).sum (λ (i : ℕ), f i) = (unique_factorization_monoid.normalized_factors n).to_finset.powerset.sum (λ (i : finset ℕ), f i.val.prod)
source
theorem nat.sq_mul_squarefree_of_pos {n : ℕ} (hn : 0 < n) :
∃ (a b : ℕ), 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ squarefree a
source
theorem nat.sq_mul_squarefree_of_pos' {n : ℕ} (h : 0 < n) :
∃ (a b : ℕ), (b + 1) ^ 2 * (a + 1) = n ∧ squarefree (a + 1)
source
theorem nat.sq_mul_squarefree (n : ℕ) :
∃ (a b : ℕ), b ^ 2 * a = n ∧ squarefree a
source
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.

Square-free prover #

source
def tactic.norm_num.squarefree_helper (n k : ℕ) :
Prop

A predicate representing partial progress in a proof of squarefree.

Equations
source
theorem tactic.norm_num.squarefree_bit10 (n : ℕ) (h : tactic.norm_num.squarefree_helper n 1) :
squarefree (bit0 (bit1 n))
source
theorem tactic.norm_num.squarefree_bit1 (n : ℕ) (h : tactic.norm_num.squarefree_helper n 1) :
squarefree (bit1 n)
source
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
source
theorem tactic.norm_num.squarefree_helper_1 (n k k' : ℕ) (e : k + 1 = k') (hk : nat.prime (bit1 k) → ¬bit1 k ∣ bit1 n) (H : tactic.norm_num.squarefree_helper n k') :
tactic.norm_num.squarefree_helper n k
source
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 : tactic.norm_num.squarefree_helper n k') :
tactic.norm_num.squarefree_helper n k
source
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 : tactic.norm_num.squarefree_helper n' k') :
tactic.norm_num.squarefree_helper n k
source
theorem tactic.norm_num.squarefree_helper_4 (n k k' : ℕ) (e : bit1 k * bit1 k = k') (hd : bit1 n < k') :
tactic.norm_num.squarefree_helper n k
source
theorem tactic.norm_num.not_squarefree_mul (a aa b n : ℕ) (ha : a * a = aa) (hb : aa * b = n) (h₁ : 1 < a) :
¬squarefree n
source
meta def tactic.norm_num.prove_non_squarefree (e : expr) (n a : ℕ) :
tactic expr

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

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

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

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

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

source
meta def tactic.norm_num.eval_squarefree  :
expr → tactic (expr × expr)

Evaluates the squarefree predicate on naturals.