Theorem ValuativeRel.exists_valuation_div_valuation_eq

Modification history

2025-10-05 10:04
Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean
feat: the definition of nonarchimedean local fields (#27465)
Added ValuativeRel.exists_valuation_div_valuation_eqView on Github →