Commit 2025-01-14 16:01 4a30ca3e

View on Github →

feat(RingTheory/Valuation): valuation integers ring is a Principal Ideal ring iff the valuation range is not densely ordered (#16619)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/Hom/Basic.lean

Created Mathlib/RingTheory/Valuation/Archimedean.lean

added theorem Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered

added theorem Valuation.Integers.wellFounded_gt_on_v_iff_discrete_mrange

added theorem Valuation.Integers.wfDvdMonoid_iff_wellFounded_gt_on_v

Modified Mathlib/RingTheory/Valuation/Basic.lean

added theorem Valuation.val_mrange_zero

Modified Mathlib/RingTheory/Valuation/Integers.lean

added theorem Valuation.Integers.bijective_algebraMap_of_subsingleton_units_mrange