Discretely valued field (source code)

= Discretely valued field

A discretely valued field is a field equipped with a <discrete valuation>. It is complete when every <Cauchy sequence> for the induced metric converges.