Polynomial_Forms_over_Field_form_Principal_Ideal_Domain

Proved

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

polynomialprincipal-ideal-domainproofwikiring-theory

Let $\struct {F, +, \circ}$ be a field whose zero is $0_F$ and whose unity is $1_F$ . Let $X$ be transcendental over $F$ . Let $F \sqbrk X$ be the ring of polynomials in $X$ over $F$ . Then $F \sqbrk X$ is a principal ideal domain.

Preamble

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

Formal statement

theorem Polynomial_Forms_over_Field_form_Principal_Ideal_Domain {F : Type _} [Field F] : IsPrincipalIdealRing (Polynomial F) := by sorry

Source

https://proofwiki.org/wiki/Polynomial_Forms_over_Field_form_Principal_Ideal_Domain

View graph