Theorem Valuation.Integers.not_denselyOrdered_of_isPrincipalIdealRing

Modification history

2024-09-17 08:32

Mathlib/RingTheory/Valuation/Integers.lean

feat(RingTheory): `Valuation.Integers.not_denselyOrdered_of_isPrincipalIdealRing` (#15939) …

Added Valuation.Integers.not_denselyOrdered_of_isPrincipalIdealRing View on Github →