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 #

squarefree r indicates that r is only divisible by x * x if x is a unit.

Main Results #

multiplicity.squarefree_iff_multiplicity_le_one: x is squarefree iff for every y, either multiplicity y x ≤ 1 or is_unit y.
unique_factorization_monoid.squarefree_iff_nodup_factors: A nonzero element x of a unique factorization monoid is squarefree iff factors x has no duplicate factors.
nat.squarefree_iff_nodup_factors: A positive natural number x is squarefree iff the list factors x has no duplicate factors.

Tags #

squarefree, multiplicity

source

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

source

@[simp]

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

squarefree x

source

@[simp]

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

squarefree 1

source

@[simp]

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

¬squarefree 0

source

@[simp]

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

squarefree x

source

@[simp]

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

squarefree x

source

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

squarefree x

source

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

source

theorem unique_factorization_monoid.squarefree_iff_nodup_factors {R : Type u_1} [comm_cancel_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.factors x).nodup

source

theorem unique_factorization_monoid.dvd_pow_iff_dvd_of_squarefree {R : Type u_1} [comm_cancel_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

source

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

squarefree n ↔ n.factors.nodup

source

@[instance]

def nat.squarefree.decidable_pred :

decidable_pred squarefree

Equations

nat.squarefree.decidable_pred (n + 1) = decidable_of_iff n.succ.factors.nodup _
nat.squarefree.decidable_pred 0 = is_false nat.squarefree.decidable_pred._main._proof_1

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.factors n).to_finset.powerset.val

source

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.factors n).to_finset.powerset, 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