addVal_def' — Mathlib

English

An integral domain with a HasUnitMulPowIrreducibleFactorization structure is a discrete valuation ring.

Русский

Целочисленное кольцо с структурой HasUnitMulPowIrreducibleFactorization является DVR.

LaTeX

$$$\mathrm{IsDiscreteValuationRing}(R)$$$

Lean4

/-- An alternative definition of the additive valuation, taking units into account -/
theorem addVal_def' (u : Rˣ) {ϖ : R} (hϖ : Irreducible ϖ) (n : ℕ) : addVal R ((u : R) * ϖ ^ n) = n :=
  addVal_def _ u hϖ n rfl

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