Documentation

Mathlib.Algebra.Squarefree.Basic

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 #

Main Results #

Tags #

squarefree, multiplicity

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

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

Equations
    Instances For
      theorem IsRelPrime.of_squarefree_mul {R : Type u_1} [CommMonoid R] {m n : R} (h : Squarefree (m * n)) :
      @[simp]
      theorem IsUnit.squarefree {R : Type u_1} [CommMonoid R] {x : R} (h : IsUnit x) :
      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) :
      @[simp]
      theorem Prime.squarefree {R : Type u_1} [CancelCommMonoidWithZero R] {x : R} (h : Prime x) :
      theorem Squarefree.of_mul_left {R : Type u_1} [Monoid R] {m n : R} (hmn : Squarefree (m * n)) :
      theorem Squarefree.of_mul_right {R : Type u_1} [CommMonoid R] {m n : R} (hmn : Squarefree (m * n)) :
      theorem Squarefree.squarefree_of_dvd {R : Type u_1} [Monoid R] {x y : R} (hdvd : x y) (hsq : 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} [CancelCommMonoidWithZero α] [GCDMonoid α] (a : α) {b : α} (hb : Squarefree b) :
      theorem Squarefree.gcd_left {α : Type u_2} [CancelCommMonoidWithZero α] [GCDMonoid α] {a : α} (b : α) (ha : Squarefree a) :
      theorem squarefree_iff_emultiplicity_le_one {R : Type u_1} [CommMonoid R] (r : R) :
      Squarefree r ∀ (x : R), emultiplicity x r 1 IsUnit x
      @[deprecated squarefree_iff_emultiplicity_le_one (since := "2024-11-30")]

      Alias of squarefree_iff_emultiplicity_le_one.

      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 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.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} [CancelCommMonoidWithZero R] {x : R} (h0 : x 0) (h : IsRadical x) :
      theorem Squarefree.pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right {R : Type u_1} [CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero R] {x y p : R} {k : } (hy : Squarefree y) (hp : Prime p) (h : p ^ (k + 1) x * y) :
      p ^ k x

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

      theorem exists_squarefree_dvd_pow_of_ne_zero {R : Type u_1} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {x : R} (hx : x 0) :
      ∃ (y : R) (n : ), Squarefree y y x x y ^ n