# mathlibdocumentation

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.

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

## 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
• = ∀ (x : R), x * x r
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} [nontrivial R] :
theorem squarefree.ne_zero {R : Type u_1} [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} {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.squarefree_iff_multiplicity_le_one {R : Type u_1} [comm_monoid R] (r : R) :
∀ (x : R), r 1
theorem multiplicity.finite_prime_left {R : Type u_1} {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} (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 unique_factorization_monoid.dvd_pow_iff_dvd_of_squarefree {R : Type u_1} [nontrivial R] {x y : R} {n : } (hsq : squarefree x) (h0 : n 0) :
x y ^ n x y