Theorem ValuativeRel.ValueGroupWithZero.mk_eq_valuation

Modification history

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