intValuation_if_neg — Mathlib

English

If r ≠ 0, then v.intValuation r equals Multiplicative.ofAdd of the negated count of prime factors of (r).

Русский

Если r ≠ 0, то v.intValuation(r) = Multiplicative.ofAdd(-count(factors( (r) )))

LaTeX

$$v.intValuation(r) = \operatorname{ofAdd}(-(\#(\text{factors}((r)))) )$$

Lean4

theorem intValuation_if_neg {r : R} (hr : r ≠ 0) :
    v.intValuation r =
      Multiplicative.ofAdd
        (-(Associates.mk v.asIdeal).count (Associates.mk (Ideal.span { r } : Ideal R)).factors : ℤ) :=
  intValuationDef_if_neg _ hr

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