mathlib

db2a972d - feat(ring_theory/principal_ideal_domain): The generator of a principal prime ideal is a prime (#6731)