ofHasUnitMulPowIrreducibleFactorization

English

An integral domain with an irreducible element p such that every nonzero element is associated to a power of p is a discrete valuation ring.

Русский

Целостное кольцо с ирредуцируемым элементом p, при котором каждое ненулевое элемент связано с степенью p, является дискретным оценочным кольцом.

LaTeX

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

Lean4

/-- An integral domain in which there is an irreducible element `p`
such that every nonzero element is associated to a power of `p`
is a discrete valuation ring.
-/
theorem ofHasUnitMulPowIrreducibleFactorization {R : Type u} [CommRing R] [IsDomain R]
    (hR : HasUnitMulPowIrreducibleFactorization R) : IsDiscreteValuationRing R :=
  by
  letI : UniqueFactorizationMonoid R := hR.toUniqueFactorizationMonoid
  apply of_ufd_of_unique_irreducible _ hR.unique_irreducible
  obtain ⟨p, hp, H⟩ := hR
  exact
    ⟨p, hp⟩
      /- If a ring is equivalent to a DVR, it is itself a DVR. -/

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