valuation — Mathlib

English

For finite residue field, the quotient 𝒪[K]/𝓂[K]^n is finite for each n.

Русский

Для конечного остаточного поля фактор-корень 𝒪[K]/𝓂[K]^n конечен для каждого n.

LaTeX

$$$$ \forall n, \; \#(\mathcal{O}_K / \mathfrak{m}_K^n) < \infty. $$$$

Lean4

/-- The valuation on a nonarchimedean normed field `K` defined as `nnnorm`. -/
def valuation : Valuation K ℝ≥0 where
  toFun := nnnorm
  map_zero' := nnnorm_zero
  map_one' := nnnorm_one
  map_mul' := nnnorm_mul
  map_add_le_max' := IsUltrametricDist.norm_add_le_max

Похожие утверждения