intValuation_def — Mathlib

English

The value of intValuation as a functor coincides with intValuationDef.

Русский

Значение intValuation как отображение совпадает с intValuationDef.

LaTeX

$$v.intValuation = intValuationDef$$

Lean4

theorem intValuation_def {r : R} :
    v.intValuation r =
      if r = 0 then 0
      else
        ↑(Multiplicative.ofAdd
            (-(Associates.mk v.asIdeal).count (Associates.mk (Ideal.span { r } : Ideal R)).factors : ℤ)) :=
  rfl

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