English
In a principal ideal ring, an irreducible element generates a maximal ideal.
Русский
В кольце с главными идеалами неприводимый элемент порождает максимальный идеал.
LaTeX
$$$p \\text{ irreducible} \\Rightarrow \\langle p \\rangle \\text{ maximal}$$$
Lean4
theorem isMaximal_of_irreducible [CommSemiring R] [IsPrincipalIdealRing R] {p : R} (hp : Irreducible p) :
Ideal.IsMaximal (span R ({ p } : Set R)) :=
⟨⟨mt Ideal.span_singleton_eq_top.1 hp.1, fun I hI =>
by
rcases principal I with ⟨a, rfl⟩
rw [Ideal.submodule_span_eq, Ideal.span_singleton_eq_top]
rcases Ideal.span_singleton_le_span_singleton.1 (le_of_lt hI) with ⟨b, rfl⟩
refine (of_irreducible_mul hp).resolve_right (mt (fun hb => ?_) (not_le_of_gt hI))
rw [Ideal.submodule_span_eq, Ideal.submodule_span_eq, Ideal.span_singleton_le_span_singleton,
IsUnit.mul_right_dvd hb]⟩⟩
