intValuation_singleton — Mathlib

English

If v.asIdeal = span{r} for some r ≠ 0, then v(r) = -1.

Русский

Если v.asIdeal = span{r} для некоторого r ≠ 0, тогда v(r) = -1.

LaTeX

$$v.asIdeal = \operatorname{span}\{r\} \Rightarrow v(r) = -1$$

Lean4

/-- The `I`-adic valuation of a generator of `I` equals `(-1 : ℤᵐ⁰)` -/
theorem intValuation_singleton {r : R} (hr : r ≠ 0) (hv : v.asIdeal = Ideal.span { r }) :
    v.intValuation r = Multiplicative.ofAdd (-1 : ℤ) := by
  classical
  rw [v.intValuation_if_neg hr, ← hv, Associates.count_self, Int.ofNat_one, ofAdd_neg, WithZero.coe_inv]
  apply v.associates_irreducible

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