English
For any r in a commutative monoid with zero, either r=0 and no irreducibles, or r is squarefree, equivalently, for every irreducible x, x^2 ∤ r.
Русский
Для любого r в коммутативном моноиде с нулём либо r=0 и нет irreducible, либо r квадратно свободен, эквивалентно: для каждого irreducible x, x^2 ∤ r.
LaTeX
$$$\bigl(\forall x, \mathrm{Irreducible}(x) \rightarrow \neg x^{2} \mid r\bigr) \iff (r = 0 \wedge \forall x, \neg \mathrm{Irreducible}(x)) \lor \mathrm{Squarefree}(r)$$$
Lean4
theorem squarefree_iff_no_irreducibles {x : R} (hx₀ : x ≠ 0) : Squarefree 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)
