addVal — Mathlib

English

Re-states that equality of exponents follows from a unit-corrected equality of powers of irreducibles.

Русский

Повторение утверждения о том, что равенство степеней следует из единично-корректного равенства степеней ирредуцируемых.

LaTeX

$$$m = n$$$

Lean4

/-- The `ℕ∞`-valued additive valuation on a DVR. -/
noncomputable def addVal (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] : AddValuation R ℕ∞ :=
  multiplicity_addValuation (Classical.choose_spec (exists_prime R))

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