isPrime_int_iff — Mathlib

English

For P : Ideal ℤ, P.IsPrime is equivalent to P = ⊥ or ∃ p ∈ ℕ prime with P = span{(p : ℤ)}.

Русский

Для P : Ideal ℤ, P.IsPrime эквивалентно P = ⊥ или ∃ p ∈ ℕ, простое, и P = span{p} в ℤ.

LaTeX

$$$P.IsPrime \iff P = ⊥ \lor \exists p : \mathbb{N}, p.Prime \land P = \mathrm{span}\{(p : \mathbb{Z})\}$$$

Lean4

theorem isPrime_int_iff {P : Ideal ℤ} : P.IsPrime ↔ P = ⊥ ∨ ∃ p : ℕ, p.Prime ∧ P = span {(p : ℤ)} :=
  isPrime_iff_of_isPrincipalIdealRing_of_noZeroDivisors.trans <|
    or_congr_right
      ⟨fun ⟨p, hp, eq⟩ ↦ ⟨_, Int.prime_iff_natAbs_prime.mp hp, eq.trans p.span_natAbs.symm⟩, fun ⟨_p, hp, eq⟩ ↦
        ⟨_, Nat.prime_iff_prime_int.mp hp, eq⟩⟩

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