irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree

English

Let r be an element in a commutative monoid with zero; if there exists an irreducible x, then (for all x irreducible, x^2 ∤ r) is equivalent to r=0 or r is squarefree.

Русский

Пусть r — элемент в коммутативном моноиде с нулём; если существует неприводимый x, тогда (для всех неприводимых x, x^2 не делит r) эквивалентно r=0 или 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 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)

Похожие утверждения