English
In a principal ideal ring, every nonzero prime ideal is maximal.
Русский
В главном кольце каждый ненулевой простой идеал максимален.
LaTeX
$$$S \\,\\text{prime} \\Rightarrow S \\\\text{is maximal}$, при условии $S \\neq 0$$$
Lean4
theorem to_maximal_ideal [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Ideal R} [hpi : IsPrime S]
(hS : S ≠ ⊥) : IsMaximal S :=
isMaximal_iff.2
⟨(ne_top_iff_one S).1 hpi.1, by
intro T x hST hxS hxT
obtain ⟨z, hz⟩ := (mem_iff_generator_dvd _).1 (hST <| generator_mem S)
cases hpi.mem_or_mem (show generator T * z ∈ S from hz ▸ generator_mem S) with
| inl h =>
have hTS : T ≤ S := by rwa [← T.span_singleton_generator, Ideal.span_le, singleton_subset_iff]
exact (hxS <| hTS hxT).elim
| inr h =>
obtain ⟨y, hy⟩ := (mem_iff_generator_dvd _).1 h
have : generator S ≠ 0 := mt (eq_bot_iff_generator_eq_zero _).2 hS
rw [← mul_one (generator S), hy, mul_left_comm, mul_right_inj' this] at hz
exact hz.symm ▸ T.mul_mem_right _ (generator_mem T)⟩
