Commit 2025-10-05 10:04 d19e914d

View on Github →

feat: the definition of nonarchimedean local fields (#27465)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/LocalField/Basic.lean

added theorem IsNonarchimedeanLocalField.isCompact_closedBall

added def IsNonarchimedeanLocalField.valueGroupWithZeroIsoInt

Modified Mathlib/RingTheory/Valuation/RankOne.lean

Modified Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean

added theorem ValuativeRel.ValueGroupWithZero.mk_eq_valuation

added theorem ValuativeRel.exists_valuation_div_valuation_eq

modified theorem ValuativeRel.isNontrivial_iff_isNontrivial

modified theorem ValuativeRel.valuation_surjective

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

added theorem IsValuativeTopology.hasBasis_nhds'

added theorem IsValuativeTopology.hasBasis_nhds_zero'

added theorem IsValuativeTopology.v_eq_valuation