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

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