Proving a Dedekind domain is a PID #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file contains some results that we can use to show all ideals in a Dedekind domain are principal.
Main results #
P be a prime ideal,
x ∈ P \ P² and
x ∉ Q for all prime ideals
Q ≠ P.
P is generated by
An invertible fractional ideal of a commutative ring with finitely many maximal ideals is principal.
An invertible ideal in a commutative ring with finitely many maximal ideals is principal.
p is a prime in the Dedekind domain
S an extension of
Sₚ the localization
p, then all primes in
Sₚ are factors of the image of
p be a prime in the Dedekind domain
S be an integral extension of
then the localization
p is a PID.