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 thatr
is only divisible byx * x
ifx
is a unit.
Main Results
multiplicity.squarefree_iff_multiplicity_le_one
:x
issquarefree
iff for everyy
, eithermultiplicity y x ≤ 1
oris_unit y
.unique_factorization_monoid.squarefree_iff_nodup_factors
: A nonzero elementx
of a unique factorization monoid is squarefree ifffactors x
has no duplicate factors.nat.squarefree_iff_nodup_factors
: A positive natural numberx
is squarefree iff the listfactors x
has no duplicate factors.Tags
squarefree, multiplicity
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]
@[simp]
@[simp]
@[simp]
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
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) :
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) :
@[instance]
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
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
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