Theorem IsValuativeTopology.v_eq_valuation

Modification history

2025-10-05 10:04
Mathlib/Topology/Algebra/Valued/ValuativeRel.lean
feat: the definition of nonarchimedean local fields (#27465)
Added IsValuativeTopology.v_eq_valuationView on Github →