Generator of a principal maximal ideal is irreducible

Stream: Is there code for X?

[Artie Khovanov]

Struggling to find the fact that a generator of a principal maximal ideal must be irreducible.
Anyone know where it might be hiding?
the special case IsDiscreteValuationRing.irreducible_of_span_eq_maximalIdeal proves the result by hand!

[Filippo A. E. Nuccio]

Well, but this is false if the ring is a field (zero is not irreducible) and if the ring is not a domain, as prime does not imply irreducible, no?

[Filippo A. E. Nuccio]

But you can do

import Mathlib

example (R : Type) [CommRing R] [IsDomain R] {M : Ideal R} {m : R} (hm : m ≠ 0) {hmM : M = Ideal.span {m}} (hM : M.IsMaximal) : Irreducible m :=
(Ideal.span_singleton_prime hm).mp (hmM ▸ hM.isPrime)|>.irreducible

[Artie Khovanov]

Filippo A. E. Nuccio said:

Well, but this is false if the ring is a field (zero is not irreducible) and if the ring is not a domain, as prime does not imply irreducible, no?

Oh maybe the definition of "irreducible" in Mathlib is bad for zero divisors. In any case thanks for this proof, I forgot it holds more generally for primes!