Squarefree elements of monoids #

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

Results about squarefree natural numbers are proved in Data.Nat.Squarefree.

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 IsUnit y.
• UniqueFactorizationMonoid.squarefree_iff_nodup_factors: A nonzero element x of a unique factorization monoid is squarefree iff factors x has no duplicate factors.

Tags #

squarefree, multiplicity

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

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

Equations
• = ∀ (x : R), x * x r
Instances For
theorem IsRelPrime.of_squarefree_mul {R : Type u_1} [] {m : R} {n : R} (h : Squarefree (m * n)) :
@[simp]
theorem IsUnit.squarefree {R : Type u_1} [] {x : R} (h : ) :
theorem squarefree_one {R : Type u_1} [] :
@[simp]
theorem not_squarefree_zero {R : Type u_1} [] [] :
theorem Squarefree.ne_zero {R : Type u_1} [] [] {m : R} (hm : ) :
m 0
@[simp]
theorem Irreducible.squarefree {R : Type u_1} [] {x : R} (h : ) :
@[simp]
theorem Prime.squarefree {R : Type u_1} {x : R} (h : ) :
theorem Squarefree.of_mul_left {R : Type u_1} [] {m : R} {n : R} (hmn : Squarefree (m * n)) :
theorem Squarefree.of_mul_right {R : Type u_1} [] {m : R} {n : R} (hmn : Squarefree (m * n)) :
theorem Squarefree.squarefree_of_dvd {R : Type u_1} [] {x : R} {y : R} (hdvd : x y) (hsq : ) :
theorem Squarefree.eq_zero_or_one_of_pow_of_not_isUnit {R : Type u_1} [] {x : R} {n : } (h : Squarefree (x ^ n)) (h' : ¬) :
n = 0 n = 1
theorem Squarefree.gcd_right {α : Type u_2} [] (a : α) {b : α} (hb : ) :
theorem Squarefree.gcd_left {α : Type u_2} [] {a : α} (b : α) (ha : ) :
theorem multiplicity.squarefree_iff_multiplicity_le_one {R : Type u_1} [] [DecidableRel Dvd.dvd] (r : R) :
∀ (x : R), 1
theorem multiplicity.finite_prime_left {R : Type u_1} [] {a : R} {b : R} (ha : ) (hb : b 0) :
theorem squarefree_iff_no_irreducibles {R : Type u_1} [] {x : R} (hx₀ : x 0) :
∀ (p : R), ¬p * p x
theorem irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree {R : Type u_1} [] (r : R) :
(∀ (x : R), ¬x * x r) (r = 0 ∀ (x : R), )
theorem squarefree_iff_irreducible_sq_not_dvd_of_ne_zero {R : Type u_1} [] {r : R} (hr : r 0) :
∀ (x : R), ¬x * x r
theorem squarefree_iff_irreducible_sq_not_dvd_of_exists_irreducible {R : Type u_1} [] {r : R} (hr : ∃ (x : R), ) :
∀ (x : R), ¬x * x r
theorem Squarefree.isRadical {R : Type u_1} {x : R} (hx : ) :
theorem Squarefree.dvd_pow_iff_dvd {R : Type u_1} {x : R} {y : R} {n : } (hsq : ) (h0 : n 0) :
x y ^ n x y
@[deprecated Squarefree.dvd_pow_iff_dvd]
theorem UniqueFactorizationMonoid.dvd_pow_iff_dvd_of_squarefree {R : Type u_1} {x : R} {y : R} {n : } (hsq : ) (h0 : n 0) :
x y ^ n x y

Alias of Squarefree.dvd_pow_iff_dvd.

theorem IsRadical.squarefree {R : Type u_1} {x : R} (h0 : x 0) (h : ) :
theorem Squarefree.pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right {R : Type u_1} {x : R} {y : R} {p : R} {k : } (hx : ) (hp : ) (h : p ^ (k + 1) x * y) :
p ^ k y
theorem Squarefree.pow_dvd_of_squarefree_of_pow_succ_dvd_mul_left {R : Type u_1} {x : R} {y : R} {p : R} {k : } (hy : ) (hp : ) (h : p ^ (k + 1) x * y) :
p ^ k x
theorem Squarefree.dvd_of_squarefree_of_mul_dvd_mul_right {R : Type u_1} {x : R} {y : R} {d : R} (hx : ) (h : d * d x * y) :
d y
theorem Squarefree.dvd_of_squarefree_of_mul_dvd_mul_left {R : Type u_1} {x : R} {y : R} {d : R} (hy : ) (h : d * d x * y) :
d x
theorem squarefree_mul_iff {R : Type u_1} {x : R} {y : R} :

x * y is square-free iff x and y have no common factors and are themselves square-free.

theorem isRadical_iff_squarefree_or_zero {R : Type u_1} {x : R} :
x = 0
theorem isRadical_iff_squarefree_of_ne_zero {R : Type u_1} {x : R} (h : x 0) :
theorem exists_squarefree_dvd_pow_of_ne_zero {R : Type u_1} {x : R} (hx : x 0) :
∃ (y : R) (n : ), y x x y ^ n
@[simp]
theorem Int.squarefree_natAbs {n : } :
Squarefree n.natAbs
@[simp]
theorem Int.squarefree_natCast {n : } :
@[deprecated Int.squarefree_natCast]
theorem Int.squarefree_coe_nat {n : } :

Alias of Int.squarefree_natCast.