Commit 2025-07-14 06:20 eb278a2b

View on Github →

feat(Valued/LocallyCompact): locally compact iff complete and DVR and finite residue field (#26549) generalized from NontriviallyNormedFields to any RankOne Valued field even though one can get a NontriviallyNormedField instance when opening a scope it's better to provide the proofs such that they work on Valued directly, like on Zm0

Estimated changes

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

modified theorem Valued.integer.compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField

modified theorem Valued.integer.isDiscreteValuationRing_of_compactSpace

modified theorem Valued.integer.isPrincipalIdealRing_of_compactSpace

modified theorem Valued.integer.properSpace_iff_compactSpace_integer

modified theorem Valued.integer.properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField

modified theorem Valued.integer.totallyBounded_iff_finite_residueField

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

added theorem Valued.toNormedField.setOf_mem_integer_eq_closedBall