mathlib documentation

def squarefree {R : Type u_1} [monoid R] (r : R) :

Prop

An element of a monoid is squarefree if the only squares that divide it are the squares of units.

Equations

squarefree r = ∀ (x : R), x * x ∣ r → is_unit x

@[simp]

theorem is_unit.squarefree {R : Type u_1} [comm_monoid R] {x : R} (h : is_unit x) :

@[simp]

theorem squarefree_one {R : Type u_1} [comm_monoid R] :

squarefree 1

@[simp]

theorem not_squarefree_zero {R : Type u_1} [monoid_with_zero R] [nontrivial R] :

¬squarefree 0

theorem squarefree.ne_zero {R : Type u_1} [monoid_with_zero R] [nontrivial R] {m : R} (hm : squarefree m) :

m ≠ 0

@[simp]

theorem irreducible.squarefree {R : Type u_1} [comm_monoid R] {x : R} (h : irreducible x) :

@[simp]

theorem prime.squarefree {R : Type u_1} [cancel_comm_monoid_with_zero R] {x : R} (h : prime x) :

theorem squarefree.of_mul_left {R : Type u_1} [comm_monoid R] {m n : R} (hmn : squarefree (m * n)) :

squarefree m

theorem squarefree.of_mul_right {R : Type u_1} [comm_monoid R] {m n : R} (hmn : squarefree (m * n)) :

squarefree n

theorem squarefree_of_dvd_of_squarefree {R : Type u_1} [comm_monoid R] {x y : R} (hdvd : x ∣ y) (hsq : squarefree y) :

theorem multiplicity.squarefree_iff_multiplicity_le_one {R : Type u_1} [comm_monoid R] [decidable_rel has_dvd.dvd] (r : R) :

squarefree r ↔ ∀ (x : R), multiplicity x r ≤ 1 ∨ is_unit x

theorem multiplicity.finite_prime_left {R : Type u_1} [cancel_comm_monoid_with_zero R] [wf_dvd_monoid R] {a b : R} (ha : prime a) (hb : b ≠ 0) :

multiplicity.finite a b

theorem irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree {R : Type u_1} [comm_monoid_with_zero R] [wf_dvd_monoid R] (r : R) :

(∀ (x : R), irreducible x → ¬x * x ∣ r) ↔ (r = 0 ∧ ∀ (x : R), ¬irreducible x) ∨ squarefree r

theorem squarefree_iff_irreducible_sq_not_dvd_of_ne_zero {R : Type u_1} [comm_monoid_with_zero R] [wf_dvd_monoid R] {r : R} (hr : r ≠ 0) :

squarefree r ↔ ∀ (x : R), irreducible x → ¬x * x ∣ r

theorem squarefree_iff_irreducible_sq_not_dvd_of_exists_irreducible {R : Type u_1} [comm_monoid_with_zero R] [wf_dvd_monoid R] {r : R} (hr : ∃ (x : R), irreducible x) :

squarefree r ↔ ∀ (x : R), irreducible x → ¬x * x ∣ r

theorem unique_factorization_monoid.squarefree_iff_nodup_normalized_factors {R : Type u_1} [cancel_comm_monoid_with_zero R] [nontrivial R] [unique_factorization_monoid R] [normalization_monoid R] [decidable_eq R] {x : R} (x0 : x ≠ 0) :

squarefree x ↔ (unique_factorization_monoid.normalized_factors x).nodup

theorem unique_factorization_monoid.dvd_pow_iff_dvd_of_squarefree {R : Type u_1} [cancel_comm_monoid_with_zero R] [nontrivial R] [unique_factorization_monoid R] [normalization_monoid R] {x y : R} {n : ℕ} (hsq : squarefree x) (h0 : n ≠ 0) :

x ∣ y ^ n ↔ x ∣ y

theorem nat.squarefree_iff_nodup_factors {n : ℕ} (h0 : n ≠ 0) :

squarefree n ↔ n.factors.nodup

theorem nat.squarefree_iff_prime_squarefree {n : ℕ} :

squarefree n ↔ ∀ (x : ℕ), nat.prime x → ¬x * x ∣ n

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

n.min_sq_fac_aux k = dite (n < k * k) (λ (h : n < k * k), none) (λ (h : ¬n < k * k), have this : nat.sqrt n + 2 - (k + 2) < nat.sqrt n + 2 - k, from _, ite (k ∣ n) (let n' : ℕ := n / k in ite (k ∣ n') (some k) (n'.min_sq_fac_aux (k + 2))) (n.min_sq_fac_aux (k + 2)))

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

n.min_sq_fac = ite (2 ∣ n) (let n' : ℕ := n / 2 in ite (2 ∣ n') (some 2) (n'.min_sq_fac_aux 3)) (n.min_sq_fac_aux 3)

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

n.min_sq_fac_prop (some d) = (nat.prime d ∧ d * d ∣ n ∧ ∀ (p : ℕ), nat.prime p → p * p ∣ n → d ≤ p)
n.min_sq_fac_prop 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_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)

theorem nat.min_sq_fac_has_prop (n : ℕ) :

n.min_sq_fac_prop n.min_sq_fac

theorem nat.min_sq_fac_prime {n d : ℕ} (h : n.min_sq_fac = some d) :

nat.prime d

theorem nat.min_sq_fac_dvd {n d : ℕ} (h : n.min_sq_fac = some d) :

d * d ∣ n

theorem nat.min_sq_fac_le_of_dvd {n d : ℕ} (h : n.min_sq_fac = some d) {m : ℕ} (m2 : 2 ≤ m) (md : m * m ∣ n) :

d ≤ m

theorem nat.squarefree_iff_min_sq_fac {n : ℕ} :

squarefree n ↔ n.min_sq_fac = none

decidable_pred squarefree

@[protected, instance]

def nat.squarefree.decidable_pred :

Equations

nat.squarefree.decidable_pred = λ (n : ℕ), decidable_of_iff' (n.min_sq_fac = none) nat.squarefree_iff_min_sq_fac

theorem nat.squarefree_two :

squarefree 2

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 : ℕ → α} :

∑ (i : ℕ) in finset.filter squarefree n.divisors, f i = ∑ (i : finset ℕ) in (unique_factorization_monoid.normalized_factors n).to_finset.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_iff_prime_sq_not_dvd (n : ℕ) :

squarefree n ↔ ∀ (x : ℕ), nat.prime x → ¬x * x ∣ n

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 #

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

Prop

A predicate representing partial progress in a proof of squarefree.

Equations

tactic.norm_num.squarefree_helper n k = (0 < k → (∀ (m : ℕ), nat.prime m → m ∣ bit1 n → bit1 k ≤ m) → squarefree (bit1 n))

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_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 : tactic.norm_num.squarefree_helper n 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 : tactic.norm_num.squarefree_helper n 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 : tactic.norm_num.squarefree_helper n' 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) :

¬squarefree n

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.

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.

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

tactic expr

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