Commit 2025-04-02 23:37 7c7049eb

View on Github →

feat(Topology/Algebra/Valued/LocallyCompact): locally compact nonarchimedean field iff complete and DVR and finite field (#16733)

Estimated changes

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

added theorem Valued.integer.compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField

added theorem Valued.integer.exists_nnnorm_lt_one

added theorem Valued.integer.exists_norm_coe_lt_one

added theorem Valued.integer.exists_norm_lt_one

added theorem Valued.integer.isDiscreteValuationRing_of_compactSpace

added theorem Valued.integer.isPrincipalIdealRing_of_compactSpace

added theorem Valued.integer.properSpace_iff_compactSpace_integer

added theorem Valued.integer.properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField

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

modified theorem Valued.integer_isOpen

added theorem Valued.isOpen_ball

added theorem Valued.isOpen_closedball

added theorem Valued.isOpen_sphere