Mathlib.Algebra.Squarefree.Basic

Squarefree definition

[Monoid R] (r : R) : Prop

Full source

/-- An element of a monoid is squarefree if the only squares that
  divide it are the squares of units. -/
def Squarefree [Monoid R] (r : R) : Prop :=
  ∀ x : R, x * x ∣ r → IsUnit x

Squarefree element of a monoid

Informal description

An element $r$ of a monoid $R$ is called *squarefree* if for any element $x \in R$, whenever $x^2$ divides $r$, then $x$ must be a unit in $R$.

IsRelPrime.of_squarefree_mul theorem

[CommMonoid R] {m n : R} (h : Squarefree (m * n)) : IsRelPrime m n

Full source

theorem IsRelPrime.of_squarefree_mul [CommMonoid R] {m n : R} (h : Squarefree (m * n)) :
    IsRelPrime m n := fun c hca hcb ↦ h c (mul_dvd_mul hca hcb)

Squarefree Product Implies Relatively Prime Elements

Informal description

Let $R$ be a commutative monoid and let $m, n \in R$. If the product $m \cdot n$ is squarefree, then $m$ and $n$ are relatively prime.

IsUnit.squarefree theorem

[CommMonoid R] {x : R} (h : IsUnit x) : Squarefree x

Full source

@[simp]
theorem IsUnit.squarefree [CommMonoid R] {x : R} (h : IsUnit x) : Squarefree x := fun _ hdvd =>
  isUnit_of_mul_isUnit_left (isUnit_of_dvd_unit hdvd h)

Units are Squarefree in a Commutative Monoid

Informal description

Let $R$ be a commutative monoid. For any unit $x \in R$, the element $x$ is squarefree.

squarefree_one theorem

[CommMonoid R] : Squarefree (1 : R)

Full source

theorem squarefree_one [CommMonoid R] : Squarefree (1 : R) :=
  isUnit_one.squarefree

Squarefreeness of the Identity Element in Commutative Monoids

Informal description

In any commutative monoid $R$, the multiplicative identity element $1$ is squarefree. That is, for any $x \in R$, if $x^2$ divides $1$, then $x$ must be a unit in $R$.

not_squarefree_zero theorem

[MonoidWithZero R] [Nontrivial R] : ¬Squarefree (0 : R)

Full source

@[simp]
theorem not_squarefree_zero [MonoidWithZero R] [Nontrivial R] : ¬Squarefree (0 : R) := by
  erw [not_forall]
  exact ⟨0, by simp⟩

Non-Squarefreeness of Zero in Nontrivial Monoids with Zero

Informal description

In a nontrivial monoid with zero $R$, the zero element $0$ is not squarefree. That is, there exists a non-unit element $x \in R$ such that $x^2$ divides $0$.

Squarefree.ne_zero theorem

[MonoidWithZero R] [Nontrivial R] {m : R} (hm : Squarefree (m : R)) : m ≠ 0

Full source

theorem Squarefree.ne_zero [MonoidWithZero R] [Nontrivial R] {m : R} (hm : Squarefree (m : R)) :
    m ≠ 0 := by
  rintro rfl
  exact not_squarefree_zero hm

Squarefree Elements are Nonzero in Nontrivial Monoids with Zero

Informal description

Let $R$ be a nontrivial monoid with zero. If an element $m \in R$ is squarefree, then $m$ is not equal to the zero element, i.e., $m \neq 0$.

Irreducible.squarefree theorem

[CommMonoid R] {x : R} (h : Irreducible x) : Squarefree x

Full source

@[simp]
theorem Irreducible.squarefree [CommMonoid R] {x : R} (h : Irreducible x) : Squarefree x := by
  rintro y ⟨z, hz⟩
  rw [mul_assoc] at hz
  rcases h.isUnit_or_isUnit hz with (hu | hu)
  · exact hu
  · apply isUnit_of_mul_isUnit_left hu

Irreducible Elements are Squarefree in Commutative Monoids

Informal description

Let $R$ be a commutative monoid. For any irreducible element $x \in R$, $x$ is squarefree. That is, if $x$ cannot be written as a product of two non-unit elements, then $x$ is not divisible by any square of a non-unit element.

Prime.squarefree theorem

[CancelCommMonoidWithZero R] {x : R} (h : Prime x) : Squarefree x

Full source

@[simp]
theorem Prime.squarefree [CancelCommMonoidWithZero R] {x : R} (h : Prime x) : Squarefree x :=
  h.irreducible.squarefree

Prime Elements are Squarefree in Cancelative Commutative Monoids with Zero

Informal description

Let $R$ be a cancelative commutative monoid with zero. For any prime element $x \in R$, $x$ is squarefree, i.e., if $x$ is prime, then for any $y \in R$, $y^2$ divides $x$ implies that $y$ is a unit.

Squarefree.of_mul_left theorem

[Monoid R] {m n : R} (hmn : Squarefree (m * n)) : Squarefree m

Full source

theorem Squarefree.of_mul_left [Monoid R] {m n : R} (hmn : Squarefree (m * n)) : Squarefree m :=
  fun p hp => hmn p (dvd_mul_of_dvd_left hp n)

Squarefree Property Preserved Under Left Multiplication

Informal description

Let $R$ be a monoid and $m, n \in R$. If the product $m \cdot n$ is squarefree, then $m$ is squarefree.

Squarefree.of_mul_right theorem

[CommMonoid R] {m n : R} (hmn : Squarefree (m * n)) : Squarefree n

Full source

theorem Squarefree.of_mul_right [CommMonoid R] {m n : R} (hmn : Squarefree (m * n)) :
    Squarefree n := fun p hp => hmn p (dvd_mul_of_dvd_right hp m)

Squarefree Property Preserved Under Right Multiplication in Commutative Monoids

Informal description

Let $R$ be a commutative monoid and let $m, n \in R$. If the product $m \cdot n$ is squarefree, then $n$ is squarefree.

Squarefree.squarefree_of_dvd theorem

[Monoid R] {x y : R} (hdvd : x ∣ y) (hsq : Squarefree y) : Squarefree x

Full source

theorem Squarefree.squarefree_of_dvd [Monoid R] {x y : R} (hdvd : x ∣ y) (hsq : Squarefree y) :
    Squarefree x := fun _ h => hsq _ (h.trans hdvd)

Squarefree elements are preserved under divisibility

Informal description

Let $R$ be a monoid and $x, y \in R$. If $x$ divides $y$ and $y$ is squarefree, then $x$ is also squarefree.

Squarefree.pow_dvd_of_pow_dvd theorem

[Monoid R] {x y : R} {n : ℕ} (hx : Squarefree y) (h : x ^ n ∣ y) : x ^ n ∣ x

Full source

theorem Squarefree.pow_dvd_of_pow_dvd [Monoid R] {x y : R} {n : ℕ}
    (hx : Squarefree y) (h : x ^ n ∣ y) : x ^ n ∣ x := by
  by_cases hu : IsUnit x
  · exact (hu.pow n).dvd
  · rcases (hx.squarefree_of_dvd h).eq_zero_or_one_of_pow_of_not_isUnit hu with rfl | rfl <;> simp

Squarefree elements satisfy $x^n \mid y \implies x^n \mid x$

Informal description

Let $R$ be a monoid and $x, y \in R$. If $y$ is squarefree and $x^n$ divides $y$ for some natural number $n$, then $x^n$ divides $x$.

Squarefree.gcd_right theorem

(a : α) {b : α} (hb : Squarefree b) : Squarefree (gcd a b)

Full source

theorem Squarefree.gcd_right (a : α) {b : α} (hb : Squarefree b) : Squarefree (gcd a b) :=
  hb.squarefree_of_dvd (gcd_dvd_right _ _)

Squarefree property preserved under right GCD in a GCD monoid

Informal description

Let $α$ be a GCD monoid and $a, b \in α$. If $b$ is squarefree, then the greatest common divisor $\gcd(a, b)$ is also squarefree.

Squarefree.gcd_left theorem

{a : α} (b : α) (ha : Squarefree a) : Squarefree (gcd a b)

Full source

theorem Squarefree.gcd_left {a : α} (b : α) (ha : Squarefree a) : Squarefree (gcd a b) :=
  ha.squarefree_of_dvd (gcd_dvd_left _ _)

Squarefree property preserved under left GCD operation

Informal description

Let $α$ be a cancelative commutative monoid with zero equipped with a GCD operation. For any elements $a, b \in α$, if $a$ is squarefree, then the greatest common divisor $\gcd(a, b)$ is also squarefree.

squarefree_iff_emultiplicity_le_one theorem

[CommMonoid R] (r : R) : Squarefree r ↔ ∀ x : R, emultiplicity x r ≤ 1 ∨ IsUnit x

Full source

theorem squarefree_iff_emultiplicity_le_one [CommMonoid R] (r : R) :
    SquarefreeSquarefree r ↔ ∀ x : R, emultiplicity x r ≤ 1 ∨ IsUnit x := by
  refine forall_congr' fun a => ?_
  rw [← sq, pow_dvd_iff_le_emultiplicity, or_iff_not_imp_left, not_le, imp_congr _ Iff.rfl]
  norm_cast
  rw [← one_add_one_eq_two]
  exact Order.add_one_le_iff_of_not_isMax (by simp)

Squarefree iff Extended Multiplicity ≤ 1 or Unit

Informal description

An element $r$ of a commutative monoid $R$ is squarefree if and only if for every element $x \in R$, either the extended multiplicity of $x$ in $r$ is at most 1, or $x$ is a unit.

squarefree_iff_no_irreducibles theorem

{x : R} (hx₀ : x ≠ 0) : Squarefree x ↔ ∀ p, Irreducible p → ¬(p * p ∣ x)

Full source

theorem squarefree_iff_no_irreducibles {x : R} (hx₀ : x ≠ 0) :
    SquarefreeSquarefree x ↔ ∀ p, Irreducible p → ¬ (p * p ∣ x) := by
  refine ⟨fun h p hp hp' ↦ hp.not_isUnit (h p hp'), fun h d hd ↦ by_contra fun hdu ↦ ?_⟩
  have hd₀ : d ≠ 0 := ne_zero_of_dvd_ne_zero (ne_zero_of_dvd_ne_zero hx₀ hd) (dvd_mul_left d d)
  obtain ⟨p, irr, dvd⟩ := WfDvdMonoid.exists_irreducible_factor hdu hd₀
  exact h p irr ((mul_dvd_mul dvd dvd).trans hd)

Squarefree iff no irreducible squares divide

Informal description

Let $x$ be a nonzero element of a monoid $R$. Then $x$ is squarefree if and only if for every irreducible element $p$ of $R$, the square $p^2$ does not divide $x$.

irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree theorem

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

Full source

theorem irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree (r : R) :
    (∀ x : R, Irreducible x → ¬x * x ∣ r) ↔ (r = 0 ∧ ∀ x : R, ¬Irreducible x) ∨ Squarefree r := by
  refine ⟨fun h ↦ ?_, ?_⟩
  · rcases eq_or_ne r 0 with (rfl | hr)
    · exact .inl (by simpa using h)
    · exact .inr ((squarefree_iff_no_irreducibles hr).mpr h)
  · rintro (⟨rfl, h⟩ | h)
    · simpa using h
    intro x hx t
    exact hx.not_isUnit (h x t)

Characterization of Squarefree Elements via Irreducibles: $(\forall x, \text{Irreducible } x \Rightarrow x^2 \nmid r) \leftrightarrow (r = 0 \land \nexists x, \text{Irreducible } x) \lor \text{Squarefree } r$

Informal description

For any element $r$ in a monoid $R$, the following are equivalent: 1. For every irreducible element $x \in R$, the square $x^2$ does not divide $r$. 2. Either $r = 0$ and there are no irreducible elements in $R$, or $r$ is squarefree.

squarefree_iff_irreducible_sq_not_dvd_of_ne_zero theorem

{r : R} (hr : r ≠ 0) : Squarefree r ↔ ∀ x : R, Irreducible x → ¬x * x ∣ r

Full source

theorem squarefree_iff_irreducible_sq_not_dvd_of_ne_zero {r : R} (hr : r ≠ 0) :
    SquarefreeSquarefree r ↔ ∀ x : R, Irreducible x → ¬x * x ∣ r := by
  simpa [hr] using (irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree r).symm

Squarefree Characterization for Nonzero Elements: $\text{Squarefree } r \leftrightarrow \forall x \text{ irreducible}, x^2 \nmid r$

Informal description

Let $r$ be a nonzero element of a monoid $R$. Then $r$ is squarefree if and only if for every irreducible element $x \in R$, the square $x^2$ does not divide $r$.

squarefree_iff_irreducible_sq_not_dvd_of_exists_irreducible theorem

{r : R} (hr : ∃ x : R, Irreducible x) : Squarefree r ↔ ∀ x : R, Irreducible x → ¬x * x ∣ r

Full source

theorem squarefree_iff_irreducible_sq_not_dvd_of_exists_irreducible {r : R}
    (hr : ∃ x : R, Irreducible x) : SquarefreeSquarefree r ↔ ∀ x : R, Irreducible x → ¬x * x ∣ r := by
  rw [irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree, ← not_exists]
  simp only [hr, not_true, false_or, and_false]

Squarefree Characterization via Irreducibles in Non-Trivial Monoids

Informal description

Let $R$ be a monoid and let $r \in R$ be an element such that there exists at least one irreducible element in $R$. Then $r$ is squarefree if and only if for every irreducible element $x \in R$, the square $x^2$ does not divide $r$.

Squarefree.isRadical theorem

{x : R} (hx : Squarefree x) : IsRadical x

Full source

theorem Squarefree.isRadical {x : R} (hx : Squarefree x) : IsRadical x :=
  (isRadical_iff_pow_one_lt 2 one_lt_two).2 fun y hy ↦ by
    obtain ⟨a, b, ha, hb, rfl⟩ := exists_dvd_and_dvd_of_dvd_mul (sq y ▸ hy)
    exact (IsRelPrime.of_squarefree_mul hx).mul_dvd ha hb

Squarefree Elements are Radical in a Monoid

Informal description

Let $R$ be a monoid and $x \in R$ a squarefree element. Then $x$ is radical, meaning that for any natural number $n$ and any element $y \in R$, if $x$ divides $y^n$, then $x$ divides $y$.

Squarefree.dvd_pow_iff_dvd theorem

{x y : R} {n : ℕ} (hsq : Squarefree x) (h0 : n ≠ 0) : x ∣ y ^ n ↔ x ∣ y

Full source

theorem Squarefree.dvd_pow_iff_dvd {x y : R} {n : ℕ} (hsq : Squarefree x) (h0 : n ≠ 0) :
    x ∣ y ^ nx ∣ y ^ n ↔ x ∣ y := ⟨hsq.isRadical n y, (·.pow h0)⟩

Squarefree Divisibility Criterion: $x \mid y^n \leftrightarrow x \mid y$ for squarefree $x$ and $n \neq 0$

Informal description

Let $R$ be a monoid, and let $x, y \in R$ with $x$ squarefree. For any nonzero natural number $n$, $x$ divides $y^n$ if and only if $x$ divides $y$.

IsRadical.squarefree theorem

(h0 : x ≠ 0) (h : IsRadical x) : Squarefree x

Full source

theorem IsRadical.squarefree (h0 : x ≠ 0) (h : IsRadical x) : Squarefree x := by
  rintro z ⟨w, rfl⟩
  specialize h 2 (z * w) ⟨w, by simp_rw [pow_two, mul_left_comm, ← mul_assoc]⟩
  rwa [← one_mul (z * w), mul_assoc, mul_dvd_mul_iff_right, ← isUnit_iff_dvd_one] at h
  rw [mul_assoc, mul_ne_zero_iff] at h0; exact h0.2

Radical Elements are Squarefree in Monoids

Informal description

Let $x$ be a nonzero element of a monoid $R$. If $x$ is radical (i.e., for every $n \in \mathbb{N}$ and $y \in R$, $x \mid y^n$ implies $x \mid y$), then $x$ is squarefree (i.e., for any $y \in R$, if $y^2$ divides $x$, then $y$ is a unit in $R$).

Squarefree.pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right theorem

{k : ℕ} (hx : Squarefree x) (hp : Prime p) (h : p ^ (k + 1) ∣ x * y) : p ^ k ∣ y

Full source

theorem pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right {k : ℕ}
    (hx : Squarefree x) (hp : Prime p) (h : p ^ (k + 1) ∣ x * y) :
    p ^ k ∣ y := by
  by_cases hxp : p ∣ x
  · obtain ⟨x', rfl⟩ := hxp
    have hx' : ¬ p ∣ x' := fun contra ↦ hp.not_unit <| hx p (mul_dvd_mul_left p contra)
    replace h : p ^ k ∣ x' * y := by
      rw [pow_succ', mul_assoc] at h
      exact (mul_dvd_mul_iff_left hp.ne_zero).mp h
    exact hp.pow_dvd_of_dvd_mul_left _ hx' h
  · exact (pow_dvd_pow _ k.le_succ).trans (hp.pow_dvd_of_dvd_mul_left _ hxp h)

Squarefree Divisibility Property: $p^{k+1} \mid x \cdot y \Rightarrow p^k \mid y$ for squarefree $x$ and prime $p$

Informal description

Let $R$ be a monoid, $x, y \in R$, $p \in R$ a prime element, and $k \in \mathbb{N}$. If $x$ is squarefree and $p^{k+1}$ divides $x \cdot y$, then $p^k$ divides $y$.

Squarefree.pow_dvd_of_squarefree_of_pow_succ_dvd_mul_left theorem

{k : ℕ} (hy : Squarefree y) (hp : Prime p) (h : p ^ (k + 1) ∣ x * y) : p ^ k ∣ x

Full source

theorem pow_dvd_of_squarefree_of_pow_succ_dvd_mul_left {k : ℕ}
    (hy : Squarefree y) (hp : Prime p) (h : p ^ (k + 1) ∣ x * y) :
    p ^ k ∣ x := by
  rw [mul_comm] at h
  exact pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right hy hp h

Squarefree Divisibility Property: $p^{k+1} \mid x \cdot y \Rightarrow p^k \mid x$ for squarefree $y$ and prime $p$

Informal description

Let $R$ be a monoid, $x, y \in R$, $p \in R$ a prime element, and $k \in \mathbb{N}$. If $y$ is squarefree and $p^{k+1}$ divides $x \cdot y$, then $p^k$ divides $x$.

Squarefree.dvd_of_squarefree_of_mul_dvd_mul_right theorem

(hx : Squarefree x) (h : d * d ∣ x * y) : d ∣ y

Full source

theorem dvd_of_squarefree_of_mul_dvd_mul_right (hx : Squarefree x) (h : d * d ∣ x * y) : d ∣ y := by
  nontriviality R
  obtain ⟨a, b, ha, hb, eq⟩ := exists_dvd_and_dvd_of_dvd_mul h
  replace ha : Squarefree a := hx.squarefree_of_dvd ha
  obtain ⟨c, hc⟩ : a ∣ d := ha.isRadical 2 d ⟨b, by rw [sq, eq]⟩
  rw [hc, mul_assoc, (mul_right_injective₀ ha.ne_zero).eq_iff] at eq
  exact dvd_trans ⟨c, by rw [hc, ← eq, mul_comm]⟩ hb

Divisibility property for squarefree elements: $d^2 \mid x \cdot y \Rightarrow d \mid y$ when $x$ is squarefree

Informal description

Let $R$ be a monoid and $x, y, d \in R$. If $x$ is squarefree and $d^2$ divides $x \cdot y$, then $d$ divides $y$.

Squarefree.dvd_of_squarefree_of_mul_dvd_mul_left theorem

(hy : Squarefree y) (h : d * d ∣ x * y) : d ∣ x

Full source

theorem dvd_of_squarefree_of_mul_dvd_mul_left (hy : Squarefree y) (h : d * d ∣ x * y) : d ∣ x :=
  dvd_of_squarefree_of_mul_dvd_mul_right hy (mul_comm x y ▸ h)

Divisibility property for squarefree elements: $d^2 \mid x \cdot y \Rightarrow d \mid x$ when $y$ is squarefree

Informal description

Let $R$ be a monoid and $x, y, d \in R$. If $y$ is squarefree and $d^2$ divides $x \cdot y$, then $d$ divides $x$.

squarefree_mul_iff theorem

: Squarefree (x * y) ↔ IsRelPrime x y ∧ Squarefree x ∧ Squarefree y

Full source

/-- `x * y` is square-free iff `x` and `y` have no common factors and are themselves square-free. -/
theorem squarefree_mul_iff : SquarefreeSquarefree (x * y) ↔ IsRelPrime x y ∧ Squarefree x ∧ Squarefree y :=
  ⟨fun h ↦ ⟨IsRelPrime.of_squarefree_mul h, h.of_mul_left, h.of_mul_right⟩,
    fun ⟨hp, sqx, sqy⟩ _ dvd ↦ hp (sqy.dvd_of_squarefree_of_mul_dvd_mul_left dvd)
      (sqx.dvd_of_squarefree_of_mul_dvd_mul_right dvd)⟩

Squarefree Product Characterization: $x \cdot y$ is squarefree $\iff$ $x$ and $y$ are relatively prime and both squarefree

Informal description

Let $x$ and $y$ be elements of a monoid. The product $x \cdot y$ is squarefree if and only if $x$ and $y$ are relatively prime and both $x$ and $y$ are squarefree.

isRadical_iff_squarefree_or_zero theorem

: IsRadical x ↔ Squarefree x ∨ x = 0

Full source

theorem isRadical_iff_squarefree_or_zero : IsRadicalIsRadical x ↔ Squarefree x ∨ x = 0 :=
  ⟨fun hx ↦ (em <| x = 0).elim .inr fun h ↦ .inl <| hx.squarefree h,
    Or.rec Squarefree.isRadical <| by
      rintro rfl
      rw [zero_isRadical_iff]
      infer_instance⟩

Characterization of Radical Elements: $\text{IsRadical}(x) \leftrightarrow \text{Squarefree}(x) \lor x = 0$

Informal description

An element $x$ of a monoid is radical if and only if it is either squarefree or equal to zero. That is, for all $x$ in the monoid, $x$ is radical (i.e., for every $n \in \mathbb{N}$ and $y$ in the monoid, $x \mid y^n$ implies $x \mid y$) if and only if either $x$ is squarefree (i.e., for any $y$ in the monoid, if $y^2$ divides $x$, then $y$ is a unit) or $x = 0$.

isRadical_iff_squarefree_of_ne_zero theorem

(h : x ≠ 0) : IsRadical x ↔ Squarefree x

Full source

theorem isRadical_iff_squarefree_of_ne_zero (h : x ≠ 0) : IsRadicalIsRadical x ↔ Squarefree x :=
  ⟨IsRadical.squarefree h, Squarefree.isRadical⟩

Characterization of Radical Elements as Squarefree Elements in Monoids

Informal description

For any nonzero element $x$ in a monoid $R$, $x$ is radical if and only if $x$ is squarefree. Here, $x$ being radical means that for any natural number $n$ and any element $y \in R$, if $x$ divides $y^n$, then $x$ divides $y$; and $x$ being squarefree means that for any element $y \in R$, if $y^2$ divides $x$, then $y$ is a unit in $R$.

exists_squarefree_dvd_pow_of_ne_zero theorem

{x : R} (hx : x ≠ 0) : ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ x ∧ x ∣ y ^ n

Full source

lemma _root_.exists_squarefree_dvd_pow_of_ne_zero {x : R} (hx : x ≠ 0) :
    ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ x ∧ x ∣ y ^ n := by
  induction x using WfDvdMonoid.induction_on_irreducible with
  | zero => contradiction
  | unit u hu => exact ⟨1, 0, squarefree_one, one_dvd u, hu.dvd⟩
  | mul z p hz hp ih =>
    obtain ⟨y, n, hy, hyx, hy'⟩ := ih hz
    rcases n.eq_zero_or_pos with rfl | hn
    · exact ⟨p, 1, hp.squarefree, dvd_mul_right p z, by simp [isUnit_of_dvd_one (pow_zero y ▸ hy')]⟩
    by_cases hp' : p ∣ y
    · exact ⟨y, n + 1, hy, dvd_mul_of_dvd_right hyx _,
        mul_comm p z ▸ pow_succ y n ▸ mul_dvd_mul hy' hp'⟩
    · suffices Squarefree (p * y) from ⟨p * y, n, this,
        mul_dvd_mul_left p hyx, mul_pow p y n ▸ mul_dvd_mul (dvd_pow_self p hn.ne') hy'⟩
      exact squarefree_mul_iff.mpr ⟨hp.isRelPrime_iff_not_dvd.mpr hp', hp.squarefree, hy⟩

Existence of Squarefree Divisor in Powers for Nonzero Elements

Informal description

For any nonzero element $x$ in a monoid $R$, there exists a squarefree element $y \in R$ and a natural number $n$ such that $y$ divides $x$ and $x$ divides $y^n$.

UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors theorem

[NormalizationMonoid R] {x : R} (x0 : x ≠ 0) : Squarefree x ↔ Multiset.Nodup (normalizedFactors x)

Full source

theorem squarefree_iff_nodup_normalizedFactors [NormalizationMonoid R] {x : R}
    (x0 : x ≠ 0) : SquarefreeSquarefree x ↔ Multiset.Nodup (normalizedFactors x) := by
  classical
  rw [squarefree_iff_emultiplicity_le_one, Multiset.nodup_iff_count_le_one]
  haveI := nontrivial_of_ne x 0 x0
  constructor <;> intro h a
  · by_cases hmem : a ∈ normalizedFactors x
    · have ha := irreducible_of_normalized_factor _ hmem
      rcases h a with (h | h)
      · rw [← normalize_normalized_factor _ hmem]
        rw [emultiplicity_eq_count_normalizedFactors ha x0] at h
        assumption_mod_cast
      · have := ha.1
        contradiction
    · simp [Multiset.count_eq_zero_of_not_mem hmem]
  · rw [or_iff_not_imp_right]
    intro hu
    rcases eq_or_ne a 0 with rfl | h0
    · simp [x0]
    rcases WfDvdMonoid.exists_irreducible_factor hu h0 with ⟨b, hib, hdvd⟩
    apply le_trans (emultiplicity_le_emultiplicity_of_dvd_left hdvd)
    rw [emultiplicity_eq_count_normalizedFactors hib x0]
    exact_mod_cast h (normalize b)

Squarefree Elements in UFDs are Characterized by Duplicate-Free Prime Factorizations

Informal description

Let $R$ be a unique factorization monoid with a normalization monoid structure. For any nonzero element $x \in R$, $x$ is squarefree if and only if the multiset of its normalized prime factors has no duplicate elements (i.e., is `Nodup`).

Int.squarefree_natAbs theorem

{n : ℤ} : Squarefree n.natAbs ↔ Squarefree n

Full source

@[simp]
theorem squarefree_natAbs {n : ℤ} : SquarefreeSquarefree n.natAbs ↔ Squarefree n := by
  simp_rw [Squarefree, natAbs_surjective.forall, ← natAbs_mul, natAbs_dvd_natAbs,
    isUnit_iff_natAbs_eq, Nat.isUnit_iff]

Squarefree Property Preserved Under Absolute Value for Integers

Informal description

For any integer $n$, the natural number obtained by taking the absolute value of $n$ is squarefree if and only if $n$ itself is squarefree in the integers. In other words, $\operatorname{natAbs}(n)$ is squarefree in $\mathbb{N}$ if and only if $n$ is squarefree in $\mathbb{Z}$.

Int.squarefree_natCast theorem

{n : ℕ} : Squarefree (n : ℤ) ↔ Squarefree n

Full source

@[simp]
theorem squarefree_natCast {n : ℕ} : SquarefreeSquarefree (n : ℤ) ↔ Squarefree n := by
  rw [← squarefree_natAbs, natAbs_natCast]

Squarefree Preservation Under Natural Number to Integer Cast

Informal description

For any natural number $n$, the integer obtained by casting $n$ to $\mathbb{Z}$ is squarefree if and only if $n$ is squarefree in $\mathbb{N}$. In other words, $n$ is squarefree as an integer if and only if it is squarefree as a natural number.

Mathlib.Algebra.Squarefree.Basic

Main Definitions

Main Results

Tags