squarefree_iff_irreducible_sq_not_dvd_of_ne_zero

English

For a monoid, if r ≠ 0, then Squarefree r is equivalent to: for all x, Irreducible x → ¬ x^2 ∣ r.

Русский

Для моноида, если r ≠ 0, то Squarefree r эквивалентно: для всех x, Irreducible x → ¬ x^2 ∣ r.

LaTeX

$$$r \neq 0 \Rightarrow \bigl(\mathrm{Squarefree}(r) \iff \forall x, \mathrm{Irreducible}(x) \rightarrow \neg x^{2} \mid r\bigr)$$$

Lean4

theorem squarefree_iff_irreducible_sq_not_dvd_of_ne_zero {r : R} (hr : r ≠ 0) :
    Squarefree 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

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