Theorem IsValuativeTopology.v_eq_valuation

Modification history

2026-06-03 06:54
Mathlib/Topology/Algebra/Valued/ValuativeRel.lean
feat(Valuation/ValuativeRel): generalize `ValuativeRel` to non-commutative rings (#36777) …
Modified IsValuativeTopology.v_eq_valuationView on Github →
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 →