mathlib documentation

algebra.squarefree

Squarefree elements of monoids #

An element of a monoid is squarefree when it is not divisible by any squares except the squares of units.

Main Definitions #

Main Results #

Tags #

squarefree, multiplicity

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
Instances for squarefree
@[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] :
@[simp]
theorem not_squarefree_zero {R : Type u_1} [monoid_with_zero R] [nontrivial R] :
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)) :
theorem squarefree.of_mul_right {R : Type u_1} [comm_monoid R] {m n : R} (hmn : squarefree (m * 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.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) :
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 nat.squarefree_iff_prime_squarefree {n : } :
squarefree n ∀ (x : ), nat.prime x¬x * x n
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) :
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
def nat.min_sq_fac (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
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
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) :
theorem nat.min_sq_fac_aux_has_prop {n : } (k : ) :
0 < n∀ (i : ), k = 2 * i + 3(∀ (m : ), nat.prime mm nk m)n.min_sq_fac_prop (n.min_sq_fac_aux k)
theorem nat.min_sq_fac_dvd {n d : } (h : n.min_sq_fac = option.some d) :
d * d n
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
theorem nat.sum_divisors_filter_squarefree {n : } (h0 : n 0) {α : Type u_1} [add_comm_monoid α] {f : → α} :
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.

Square-free prover #

A predicate representing partial progress in a proof of squarefree.

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

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

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

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

Evaluates the prime and min_fac functions.