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 : R} {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} [CommMonoid R] {m : R} {n : R} (hmn : Squarefree (m * n)) :
    theorem Squarefree.of_mul_right {R : Type u_1} [CommMonoid R] {m : R} {n : R} (hmn : Squarefree (m * n)) :
    theorem Squarefree.squarefree_of_dvd {R : Type u_1} [CommMonoid R] {x : R} {y : R} (hdvd : x y) (hsq : Squarefree y) :
    theorem Squarefree.eq_zero_or_one_of_pow_of_not_isUnit {R : Type u_1} [CommMonoid R] {x : R} {n : } (h : Squarefree (x ^ n)) (h' : ¬IsUnit x) :
    n = 0 n = 1
    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 multiplicity.finite_prime_left {R : Type u_1} [CancelCommMonoidWithZero R] [WfDvdMonoid R] {a : R} {b : R} (ha : Prime a) (hb : b 0) :
    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 : R} {y : R} {n : } (hsq : Squarefree x) (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} [CommMonoidWithZero R] [DecompositionMonoid R] {x : R} {y : R} {n : } (hsq : Squarefree x) (h0 : n 0) :
    x y ^ n x y

    Alias of Squarefree.dvd_pow_iff_dvd.

    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 : R} {y : R} {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 : R} {y : R} {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} [CancelCommMonoidWithZero R] {x : R} {y : R} {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} [CancelCommMonoidWithZero R] {x : R} {y : R} {d : R} [DecompositionMonoid R] (hy : Squarefree y) (h : d * d x * y) :
    d 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