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 #

Tags #

squarefree, multiplicity

theorem Nat.squarefree_iff_nodup_primeFactorsList {n : } (h0 : n 0) :
Squarefree n n.primeFactorsList.Nodup
@[deprecated Nat.squarefree_iff_nodup_primeFactorsList]
theorem Nat.squarefree_iff_nodup_factors {n : } (h0 : n 0) :
Squarefree n n.primeFactorsList.Nodup

Alias of Nat.squarefree_iff_nodup_primeFactorsList.

theorem Squarefree.nodup_primeFactorsList {n : } (hn : Squarefree n) :
n.primeFactorsList.Nodup
@[deprecated Squarefree.nodup_primeFactorsList]
theorem Squarefree.nodup_factors {n : } (hn : Squarefree n) :
n.primeFactorsList.Nodup

Alias of Squarefree.nodup_primeFactorsList.

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 : Nat.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 : ), Nat.Prime p(p n p m)
theorem Nat.squarefree_pow_iff {n : } {k : } (hn : n 1) (hk : k 0) :
@[irreducible]

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

    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 let n' := n / 2; if 2 n' then some 2 else n'.minSqFacAux 3 else n.minSqFacAux 3
    Instances For

      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 : Nat.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 : ), Nat.Prime mm nk 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
        Equations
        theorem Nat.divisors_filter_squarefree_of_squarefree {n : } (hn : Squarefree n) :
        Finset.filter Squarefree n.divisors = n.divisors
        theorem Nat.divisors_filter_squarefree {n : } (h0 : n 0) :
        (Finset.filter Squarefree n.divisors).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 : α} :
        iFinset.filter Squarefree n.divisors, f i = 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 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)) :
        m.Coprime 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) :
        pn.primeFactors, p = n
        theorem Nat.primeFactors_prod {s : Finset } (hs : ps, Nat.Prime p) :
        (ps, 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 ) => ps, p) {s : Finset | ps, Nat.Prime p} {n : | Squarefree n}
        theorem Nat.prod_primeFactors_sdiff_of_squarefree {n : } (hn : Squarefree n) {t : Finset } (ht : t n.primeFactors) :
        an.primeFactors \ t, a = n / at, a