English
In the ring of natural numbers, a prime ideal is either the zero ideal, or the maximal ideal, or a principal ideal generated by a prime p: P.IsPrime ⇔ P = ⊥ ∨ P = maximalIdeal ℕ ∨ ∃ p ∈ ℕ, p.Prime ∧ P = span{ p }.
Русский
В кольце ℕ простой идеал либо нулевой, либо максимальный, либо порожденный простым числом p: P IsPrime ↔ P = ⊥ ∨ P = maximalIdeal ℕ ∨ ∃ p ∈ ℕ, p Prime ∧ P = span{p}.
LaTeX
$$$P.IsPrime \iff P = \perp \ \lor\ \Big( P = \maximalIdeal \mathbb{N} \lor \ exists p\in \mathbb{N}, p\text{ Prime } \land P = \mathrm{span}\{p\} \Big)$$$
Lean4
theorem isPrime_nat_iff {P : Ideal ℕ} : P.IsPrime ↔ P = ⊥ ∨ P = maximalIdeal ℕ ∨ ∃ p : ℕ, p.Prime ∧ P = span { p } :=
by
refine
.symm
⟨?_, fun h ↦
or_iff_not_imp_left.mpr fun h0 ↦
or_iff_not_imp_right.mpr fun hsp ↦ (le_maximalIdeal h.ne_top).antisymm fun n hn ↦ ?_⟩
· rintro (rfl | rfl | ⟨p, hp, rfl⟩)
· exact bot_prime
· exact (maximalIdeal.isMaximal ℕ).isPrime
· rwa [span_singleton_prime (by simp [hp.ne_zero]), ← Nat.prime_iff]
rw [← le_bot_iff, SetLike.not_le_iff_exists] at h0
classical
let p := Nat.find h0
have ⟨(hp : p ∈ P), (hp0 : p ≠ 0)⟩ := Nat.find_spec h0
have : p ≠ 1 := ne_of_mem_of_not_mem hp P.one_notMem
have prime : p.Prime :=
Nat.prime_iff_not_exists_mul_eq.mpr <|
.intro (by cutsat) fun ⟨m, n, hm, hn, eq⟩ ↦
have := mul_ne_zero_iff.mp (eq ▸ hp0)
(h.mem_or_mem (eq ▸ hp)).elim (Nat.find_min h0 hm ⟨·, this.1⟩) (Nat.find_min h0 hn ⟨·, this.2⟩)
push_neg at hsp
have ⟨q, hq, hqp⟩ := SetLike.exists_of_lt ((P.span_singleton_le_iff_mem.mpr hp).lt_of_ne (hsp p prime).symm)
obtain rfl | hn1 := eq_or_ne n 0
· exact Ideal.zero_mem _
have : n ≠ 1 := Nat.mem_maximalIdeal_iff.mp hn
have ⟨a, b, eq⟩ :=
Nat.exists_add_mul_eq_of_gcd_dvd_of_mul_pred_le p q _
(by simp [prime.coprime_iff_not_dvd.mpr (Ideal.mem_span_singleton.not.mp hqp)])
(Nat.lt_pow_self (show 1 < n by cutsat)).le
exact h.mem_of_pow_mem _ (eq ▸ add_mem (P.mul_mem_left _ hp) (P.mul_mem_left _ hq))
