Mathlib Changelog
v4
Changelog
About
Github
Theorem
Valuation.Integers.isPrincipal_iff_exists_isGreatest
Modification history
2024-09-17 08:32
Mathlib/RingTheory/Valuation/Integers.lean
feat(RingTheory): `Valuation.Integers.not_denselyOrdered_of_isPrincipalIdealRing` (#15939) …
Added
Valuation.Integers.isPrincipal_iff_exists_isGreatest
View on Github →