valuation — Mathlib

English

The function valuation: ℚ_p → ℤ is the p-adic valuation lifted to ℚ_p.

Русский

Функция valuation: ℚ_p → ℤ — это подъём p-адической оценки к ℚ_p.

LaTeX

$$$\\mathrm{valuation}: \\mathbb{Q}_p \\to \\mathbb{Z}$$$

Lean4

/-- `Padic.valuation` lifts the `p`-adic valuation on rationals to `ℚ_[p]`. -/
def valuation : ℚ_[p] → ℤ :=
  Quotient.lift (@PadicSeq.valuation p _) fun f g h ↦
    by
    by_cases hf : f ≈ 0
    · have hg : g ≈ 0 := Setoid.trans (Setoid.symm h) hf
      simp [hf, hg, PadicSeq.valuation]
    · have hg : ¬g ≈ 0 := fun hg ↦ hf (Setoid.trans h hg)
      rw [PadicSeq.val_eq_iff_norm_eq hf hg]
      exact PadicSeq.norm_equiv h

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