Principal_Ideal_Domain_is_Unique_Factorization_Domain

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

principal-ideal-domainproofwikiring-theoryunique-factorization

Every principal ideal domain is a unique factorization domain.

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.RingTheory.PrincipalIdealDomain

Formal statement

theorem Principal_Ideal_Domain_is_Unique_Factorization_Domain {R : Type _} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] : UniqueFactorizationMonoid R := by sorry

Source

https://proofwiki.org/wiki/Principal_Ideal_Domain_is_Unique_Factorization_Domain

View graph