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

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

Instances for squarefree

nat.squarefree.decidable_pred

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

theorem squarefree.ne_zero {R : Type u_1} [monoid_with_zero R] [nontrivial R] {m : R} (hm : squarefree m) :

m ≠ 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} [cancel_comm_monoid_with_zero R] {x : R} (h : prime x) :

squarefree x

source

theorem squarefree.of_mul_left {R : Type u_1} [comm_monoid R] {m n : R} (hmn : squarefree (m * n)) :

squarefree m

source

theorem squarefree.of_mul_right {R : Type u_1} [comm_monoid R] {m n : R} (hmn : squarefree (m * n)) :

squarefree n

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 multiplicity.finite_prime_left {R : Type u_1} [cancel_comm_monoid_with_zero R] [wf_dvd_monoid R] {a b : R} (ha : prime a) (hb : b ≠ 0) :

multiplicity.finite a b

source

theorem irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree {R : Type u_1} [comm_monoid_with_zero R] [wf_dvd_monoid R] (r : R) :

(∀ (x : R), irreducible x → ¬x * x ∣ r) ↔ (r = 0 ∧ ∀ (x : R), ¬irreducible x) ∨ squarefree r

source

theorem squarefree_iff_irreducible_sq_not_dvd_of_ne_zero {R : Type u_1} [comm_monoid_with_zero R] [wf_dvd_monoid R] {r : R} (hr : r ≠ 0) :

squarefree r ↔ ∀ (x : R), irreducible x → ¬x * x ∣ r

source

theorem squarefree_iff_irreducible_sq_not_dvd_of_exists_irreducible {R : Type u_1} [comm_monoid_with_zero R] [wf_dvd_monoid R] {r : R} (hr : ∃ (x : R), irreducible x) :

squarefree r ↔ ∀ (x : R), irreducible x → ¬x * x ∣ r

source

theorem unique_factorization_monoid.squarefree_iff_nodup_normalized_factors {R : Type u_1} [cancel_comm_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.normalized_factors x).nodup

source

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