Commit 2024-11-07 22:07 e438eb2e
View on Github →chore(RingTheory/PrincipalIdealDomain): split off PrincipalIdealRing.of_prime (#18731)
This declaration pulls in a lot of ideal constructions which we don't use in e.g. the LinearAlgebra bits of the library.
(Note that this should be more impressive in combination with splitting off RingTheory.Nilpotent.Lemmas from Mathlib.RingTheory.Noetherian.)