Commit 2025-07-31 22:37 f88671b2

View on Github →

feat(Valued/LocallyCompact): do not require RankOne to show IsDVR (#27412) for isDiscreteValuationRing_of_compactSpace for the CFT workshop

Estimated changes

Modified Mathlib/GroupTheory/ArchimedeanDensely.lean

added theorem Units.mulArchimedean_iff

Modified Mathlib/Order/Basic.lean

modified theorem Subsingleton.instDenselyOrdered

Modified Mathlib/Topology/Algebra/Valued/LocallyCompact.lean

modified theorem Valued.integer.isDiscreteValuationRing_of_compactSpace

modified theorem Valued.integer.isPrincipalIdealRing_of_compactSpace

added theorem Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integer

added theorem Valued.integer.mulArchimedean_mrange_of_isCompact_integer