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_emultiplicity_le_one: x is Squarefree iff for every y, either emultiplicity 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} [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 → IsUnit x

theorem IsRelPrime.of_squarefree_mul {R : Type u_1} [CommMonoid R] {m n : R} (h : Squarefree (m * n)) : IsRelPrime m n

@[simp]

theorem IsUnit.squarefree {R : Type u_1} [CommMonoid R] {x : R} (h : IsUnit x) : Squarefree x

theorem squarefree_one {R : Type u_1} [CommMonoid R] : Squarefree 1

@[simp]

theorem not_squarefree_zero {R : Type u_1} [MonoidWithZero R] [Nontrivial R] : ¬Squarefree 0

theorem Squarefree.ne_zero {R : Type u_1} [MonoidWithZero R] [Nontrivial R] {m : R} (hm : Squarefree m) : m ≠ 0

@[simp]

theorem Irreducible.squarefree {R : Type u_1} [CommMonoid R] {x : R} (h : Irreducible x) : Squarefree x

@[simp]

theorem Prime.squarefree {R : Type u_1} [CommMonoidWithZero R] [IsCancelMulZero R] {x : R} (h : Prime x) : Squarefree x

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

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

theorem Squarefree.squarefree_of_dvd {R : Type u_1} [Monoid R] {x y : R} (hdvd : x ∣ y) (hsq : Squarefree y) : Squarefree x

theorem Associated.squarefree_iff {R : Type u_1} [Monoid R] {x y : R} (h : Associated x y) : Squarefree x ↔ Squarefree y

theorem Squarefree.eq_zero_or_one_of_pow_of_not_isUnit {R : Type u_1} [Monoid R] {x : R} {n : ℕ} (h : Squarefree (x ^ n)) (h' : ¬IsUnit x) : n = 0 ∨ n = 1

theorem Squarefree.pow_dvd_of_pow_dvd {R : Type u_1} [Monoid R] {x y : R} {n : ℕ} (hx : Squarefree y) (h : x ^ n ∣ y) : x ^ n ∣ x

theorem Squarefree.gcd_right {α : Type u_2} [CommMonoidWithZero α] [GCDMonoid α] (a : α) {b : α} (hb : Squarefree b) : Squarefree (gcd a b)

theorem Squarefree.gcd_left {α : Type u_2} [CommMonoidWithZero α] [GCDMonoid α] {a : α} (b : α) (ha : Squarefree a) : Squarefree (gcd a b)

theorem squarefree_iff_emultiplicity_le_one {R : Type u_1} [CommMonoid R] (r : R) : Squarefree r ↔ ∀ (x : R), emultiplicity x r ≤ 1 ∨ IsUnit x

theorem squarefree_iff_no_irreducibles {R : Type u_1} [CommMonoidWithZero R] [WfDvdMonoid R] {x : R} (hx₀ : x ≠ 0) : Squarefree x ↔ ∀ (p : R), Irreducible p → ¬p * p ∣ x

theorem irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree {R : Type u_1} [CommMonoidWithZero R] [WfDvdMonoid R] (r : R) : (∀ (x : R), Irreducible x → ¬x * x ∣ r) ↔ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r

theorem squarefree_iff_irreducible_sq_not_dvd_of_ne_zero {R : Type u_1} [CommMonoidWithZero R] [WfDvdMonoid R] {r : R} (hr : r ≠ 0) : Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r

theorem squarefree_iff_irreducible_sq_not_dvd_of_exists_irreducible {R : Type u_1} [CommMonoidWithZero R] [WfDvdMonoid R] {r : R} (hr : ∃ (x : R), Irreducible x) : Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r

theorem Squarefree.isRadical {R : Type u_1} [CommMonoidWithZero R] [DecompositionMonoid R] {x : R} (hx : Squarefree x) : IsRadical x

theorem Squarefree.dvd_pow_iff_dvd {R : Type u_1} [CommMonoidWithZero R] [DecompositionMonoid R] {x y : R} {n : ℕ} (hsq : Squarefree x) (h0 : n ≠ 0) : x ∣ y ^ n ↔ x ∣ y

theorem IsRadical.squarefree {R : Type u_1} [CommMonoidWithZero R] [IsCancelMulZero R] {x : R} (h0 : x ≠ 0) (h : IsRadical x) : Squarefree x

theorem Squarefree.pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right {R : Type u_1} [CommMonoidWithZero R] [IsCancelMulZero R] {x y p : R} {k : ℕ} (hx : Squarefree x) (hp : Prime p) (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} [CommMonoidWithZero R] [IsCancelMulZero R] {x y p : R} {k : ℕ} (hy : Squarefree y) (hp : Prime p) (h : p ^ (k + 1) ∣ x * y) : p ^ k ∣ x

theorem Squarefree.dvd_of_squarefree_of_mul_dvd_mul_right {R : Type u_1} [CommMonoidWithZero R] [IsCancelMulZero R] {x y d : R} [DecompositionMonoid R] (hx : Squarefree x) (h : d * d ∣ x * y) : d ∣ y

theorem Squarefree.dvd_of_squarefree_of_mul_dvd_mul_left {R : Type u_1} [CommMonoidWithZero R] [IsCancelMulZero R] {x y d : R} [DecompositionMonoid R] (hy : Squarefree y) (h : d * d ∣ x * y) : d ∣ x

theorem Squarefree.dvd_of_isSquare_mul {R : Type u_1} [CommMonoidWithZero R] [IsCancelMulZero R] {x y : R} [DecompositionMonoid R] (hx : Squarefree x) (h : IsSquare (x * y)) : x ∣ y

If x is squarefree and x * y is a square, then x ∣ y.

theorem Squarefree.associated_of_isSquare_mul {R : Type u_1} [CommMonoidWithZero R] [IsCancelMulZero R] {x y : R} [DecompositionMonoid R] (hx : Squarefree x) (hy : Squarefree y) (h : IsSquare (x * y)) : Associated x y

Two squarefree elements whose product is a square are associated.

theorem squarefree_mul_iff {R : Type u_1} [CommMonoidWithZero R] [IsCancelMulZero R] {x y : R} [DecompositionMonoid R] : Squarefree (x * y) ↔ IsRelPrime x y ∧ Squarefree x ∧ Squarefree y

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

theorem Finset.squarefree_prod_of_pairwise_isCoprime {R : Type u_1} [CommMonoidWithZero R] [IsCancelMulZero R] [DecompositionMonoid R] {ι : Type u_2} {s : Finset ι} {f : ι → R} (hs : (↑s).Pairwise (Function.onFun IsRelPrime f)) (hs' : ∀ i ∈ s, Squarefree (f i)) : Squarefree (∏ i ∈ s, f i)

theorem isRadical_iff_squarefree_or_zero {R : Type u_1} [CommMonoidWithZero R] [IsCancelMulZero R] {x : R} [DecompositionMonoid R] : IsRadical x ↔ Squarefree x ∨ x = 0

theorem isRadical_iff_squarefree_of_ne_zero {R : Type u_1} [CommMonoidWithZero R] [IsCancelMulZero R] {x : R} [DecompositionMonoid R] (h : x ≠ 0) : IsRadical x ↔ Squarefree x

theorem exists_squarefree_dvd_pow_of_ne_zero {R : Type u_1} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] {x : R} (hx : x ≠ 0) : ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ x ∧ x ∣ y ^ n

theorem exists_sq_mul_squarefree {R : Type u_1} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] (x : R) : ∃ (e : R) (d : R), e ^ 2 * d = x ∧ Squarefree d

Every element of a unique factorization monoid is a square times a squarefree element.

theorem IsSquare.of_mul_right {R : Type u_1} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] {x y : R} (hy : y ≠ 0) (h : IsSquare (x * y)) (hy' : IsSquare y) : IsSquare x

A nonzero square factor can be cancelled from a square.

theorem UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors {R : Type u_1} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] [NormalizationMonoid R] {x : R} (x0 : x ≠ 0) : Squarefree x ↔ (normalizedFactors x).Nodup

@[simp]

theorem Int.squarefree_natAbs {n : ℤ} : Squarefree n.natAbs ↔ Squarefree n

@[simp]

theorem Int.squarefree_natCast {n : ℕ} : Squarefree ↑n ↔ Squarefree n