Squarefree elements of monoids #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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 rindicates thatris only divisible byx * xifxis a unit.
Main Results #
multiplicity.squarefree_iff_multiplicity_le_one:xissquarefreeiff for everyy, eithermultiplicity y x ≤ 1oris_unit y.unique_factorization_monoid.squarefree_iff_nodup_factors: A nonzero elementxof a unique factorization monoid is squarefree ifffactors xhas no duplicate factors.
Tags #
squarefree, multiplicity
An element of a monoid is squarefree if the only squares that divide it are the squares of units.
Instances for squarefree
@[simp]
@[simp]
theorem
squarefree.ne_zero
{R : Type u_1}
[monoid_with_zero R]
[nontrivial R]
{m : R}
(hm : squarefree m) :
m ≠ 0
@[simp]
@[simp]
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.squarefree_of_dvd
{R : Type u_1}
[comm_monoid R]
{x y : R}
(hdvd : x ∣ y)
(hsq : squarefree y) :
theorem
squarefree.gcd_right
{α : Type u_2}
[cancel_comm_monoid_with_zero α]
[gcd_monoid α]
(a : α)
{b : α}
(hb : squarefree b) :
squarefree (gcd_monoid.gcd a b)
theorem
squarefree.gcd_left
{α : Type u_2}
[cancel_comm_monoid_with_zero α]
[gcd_monoid α]
{a : α}
(b : α)
(ha : squarefree a) :
squarefree (gcd_monoid.gcd a b)
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
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) :
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
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
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
theorem
is_radical.squarefree
{R : Type u_1}
[cancel_comm_monoid_with_zero R]
{x : R}
(h0 : x ≠ 0)
(h : is_radical x) :
theorem
squarefree.is_radical
{R : Type u_1}
[cancel_comm_monoid_with_zero R]
[gcd_monoid R]
{x : R}
(hx : squarefree x) :
theorem
is_radical_iff_squarefree_or_zero
{R : Type u_1}
[cancel_comm_monoid_with_zero R]
[gcd_monoid R]
{x : R} :
is_radical x ↔ squarefree x ∨ x = 0
theorem
is_radical_iff_squarefree_of_ne_zero
{R : Type u_1}
[cancel_comm_monoid_with_zero R]
[gcd_monoid R]
{x : R}
(h : x ≠ 0) :
is_radical x ↔ squarefree x
theorem
unique_factorization_monoid.squarefree_iff_nodup_normalized_factors
{R : Type u_1}
[cancel_comm_monoid_with_zero R]
[unique_factorization_monoid R]
[normalization_monoid R]
[decidable_eq R]
{x : R}
(x0 : x ≠ 0) :
theorem
unique_factorization_monoid.dvd_pow_iff_dvd_of_squarefree
{R : Type u_1}
[cancel_comm_monoid_with_zero R]
[unique_factorization_monoid R]
{x y : R}
{n : ℕ}
(hsq : squarefree x)
(h0 : n ≠ 0) :