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 numberx
is squarefree iff the listfactors x
has no duplicate factors.
Tags #
squarefree, multiplicity
theorem
nat.squarefree.factorization_le_one
{n : ℕ}
(p : ℕ)
(hn : squarefree 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_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 ∧ is_prime_pow n ↔ nat.prime n
Assuming that n
has no factors less than k
, returns the smallest prime p
such that
p^2 ∣ 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
- n.min_sq_fac = ite (2 ∣ n) (let n' : ℕ := n / 2 in ite (2 ∣ n') (option.some 2) (n'.min_sq_fac_aux 3)) (n.min_sq_fac_aux 3)
The correctness property of the return value of min_sq_fac
.
- If
none
, thenn
is squarefree; - If
some d
, thend
is a minimal square factor ofn
Equations
- n.min_sq_fac_prop (option.some d) = (nat.prime d ∧ d * d ∣ n ∧ ∀ (p : ℕ), nat.prime p → p * p ∣ n → d ≤ p)
- n.min_sq_fac_prop option.none = squarefree n
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
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
@[protected, instance]
Equations
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
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)
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 #
A predicate representing partial progress in a proof of squarefree
.
theorem
tactic.norm_num.squarefree_bit10
(n : ℕ)
(h : tactic.norm_num.squarefree_helper n 1) :
squarefree (bit0 (bit1 n))
theorem
tactic.norm_num.squarefree_bit1
(n : ℕ)
(h : tactic.norm_num.squarefree_helper n 1) :
squarefree (bit1 n)
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') :