squarefree_iff_irreducible_sq_not_dvd_of_exists_irreducible

English

Let Exists x, Irreducible x. Then Squarefree r is equivalent to: for all x, Irreducible x → ¬ x^2 ∣ r.

Русский

Пусть существует x, Irreducible x. Тогда Squarefree r эквивалентно: для всех x, Irreducible x → не делит x^2 r.

LaTeX

$$$\exists x\, \mathrm{Irreducible}(x) \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_exists_irreducible {r : R} (hr : ∃ x : R, Irreducible x) :
    Squarefree 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]

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