exists_prime_iff — Mathlib

English

There exists a prime element if and only if there exists a nonzero nonunit element.

Русский

Существует простая компонента тогда и только тогда, когда существует не нулевой неединичный элемент.

LaTeX

$$$\exists p\, \mathrm{Prime}(p) \;\Leftrightarrow\; \exists x\, (x \neq 0 \land \lnot \mathrm{IsUnit}(x)).$$$

Lean4

theorem exists_prime_iff : (∃ (p : α), Prime p) ↔ ∃ (x : α), x ≠ 0 ∧ ¬IsUnit x :=
  by
  refine ⟨fun ⟨p, hp⟩ ↦ ⟨p, hp.ne_zero, hp.not_unit⟩, fun ⟨x, hx₀, hxu⟩ ↦ ?_⟩
  obtain ⟨f, hf, -⟩ := WfDvdMonoid.exists_irreducible_factor hxu hx₀
  exact ⟨f, UniqueFactorizationMonoid.irreducible_iff_prime.mp hf⟩

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