HasUnitMulPowIrreducibleFactorization

English

If a DVR has a unit times irreducible factorization property, then it is a Unique Factorization Domain (UFD).

Русский

Если DVR обладает свойством единственной факторизации до единицы и ирредуцируемых, то это UFD.

LaTeX

$$$UniqueFactorizationMonoid R \Rightarrow HasUnitMulPowIrreducibleFactorization R \Rightarrow UniqueFactorizationMonoid R$$$

Lean4

/-- Alternative characterisation of discrete valuation rings. -/
def HasUnitMulPowIrreducibleFactorization [CommRing R] : Prop :=
  ∃ p : R, Irreducible p ∧ ∀ {x : R}, x ≠ 0 → ∃ n : ℕ, Associated (p ^ n) x

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