to_uniqueFactorizationMonoid — Mathlib

English

A principal ideal domain has unique factorization.

Русский

Главное кольцо имеет уникальное разложение на irreducible элементы.

LaTeX

$$$UniqueFactorizationMonoid(R)$$$

Lean4

/-- A principal ideal domain has unique factorization -/
instance (priority := 100) to_uniqueFactorizationMonoid : UniqueFactorizationMonoid R :=
  { (IsNoetherianRing.wfDvdMonoid : WfDvdMonoid R) with irreducible_iff_prime := irreducible_iff_prime }

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