intValuation — Mathlib

English

There exists a v-adic valuation intValuation on R with value group equal to the zero-padded integers, whose restriction to R agrees with v.intValuationDef.

Русский

Существует v-адическая оценка intValuation на R со значимой группой ℤ⁰, чья ограничение на R совпадает с v.intValuationDef.

LaTeX

$$\exists \text{val} : \mathrm{Valuation}(R, \mathbb{Z}^{\circ}) \text{ с } \text{toFun} = v.intValuationDef$$

Lean4

/-- The `v`-adic valuation on `R`. -/
def intValuation : Valuation R ℤᵐ⁰ where
  toFun := v.intValuationDef
  map_zero' := intValuation.map_zero' v
  map_one' := intValuation.map_one' v
  map_mul' := intValuation.map_mul' v
  map_add_le_max' := intValuation.map_add_le_max' v

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