valuationOfNeZero_eq — Mathlib

English

The multiplicative v-adic valuation computed by valuationOfNeZeroToFun agrees with the standard v-valuation on K for units.

Русский

Умножаемая v-адическая оценка, полученная через valuationOfNeZeroToFun, совпадает со стандартной v-оценкой на K для единиц.

LaTeX

$$(v.valuationOfNeZeroToFun x : \mathbb{Z}^{\times}) = v.valuation(K)(x)$$

Lean4

@[simp]
theorem valuationOfNeZero_eq (x : Kˣ) : (v.valuationOfNeZero x : ℤᵐ⁰) = v.valuation K x :=
  valuationOfNeZeroToFun_eq v x

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