Commit 2024-09-17 08:32 e7b3fc05

View on Github →

feat(RingTheory): Valuation.Integers.not_denselyOrdered_of_isPrincipalIdealRing (#15939) On the way to the iff when the range of valuation on nonzeros is MulArchimedean.

Estimated changes

Modified Mathlib/RingTheory/Ideal/Basic.lean

added theorem Ideal.mem_of_dvd

Modified Mathlib/RingTheory/Valuation/Integers.lean

added theorem Valuation.Integers.isPrincipal_iff_exists_isGreatest

added theorem Valuation.Integers.not_denselyOrdered_of_isPrincipalIdealRing