valuation — Mathlib

English

The valuation function on the Selmer group is defined componentwise by the valuations at each place in S.

Русский

Функция оценки в группе Selmer задаётся по компонентам на каждой точке в S.

LaTeX

$$valuation : K⟮S,n⟯ →* S → Multiplicative (ZMod n)$$

Lean4

/-- The multiplicative `v`-adic valuations on `K⟮S, n⟯` for all `v ∈ S`. -/
def valuation : K⟮S,n⟯ →* S → Multiplicative (ZMod n)
    where
  toFun x v := (v : HeightOneSpectrum R).valuationOfNeZeroMod n (x : K / n)
  map_one' := funext fun _ => map_one _
  map_mul' x y := by simp only [Subgroup.coe_mul, map_mul]; rfl

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