valuationOfNeZero — Mathlib

English

There is a multiplicative valuation from Units K to Multiplicative Z, compatible with the v-adic valuations described above, giving a global valuation across all places in S.

Русский

Существуют умножаемые отображение от единиц K к Multiplicative Z, согласующее вышеописанную v-адическую оценку, обеспечивая глобальную оценку по всем местам из S.

LaTeX

$$$\text{valuation}:\,\mathrm{Units}(K) \to (\text{Multiplicative}(\mathbb{Z}))$$$

Lean4

/-- The multiplicative `v`-adic valuation on `Kˣ`. -/
def valuationOfNeZero : Kˣ →* Multiplicative ℤ
    where
  toFun := v.valuationOfNeZeroToFun
  map_one' := by rw [← WithZero.coe_inj, valuationOfNeZeroToFun_eq]; exact map_one _
  map_mul' _
    _ := by
    rw [← WithZero.coe_inj, WithZero.coe_mul]
    simp only [valuationOfNeZeroToFun_eq]; exact map_mul _ _ _

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