Principal_Ideals_in_Integral_Domain

Proved

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

idealsintegral-domainproofwikiring-theory

Let $\struct {D, +, \circ}$ be an integral domain. Let $U_D$ be the group of units of $D$ . Let $\ideal x$ be the principal ideal of $D$ generated by $x$ . Let $x, y \in \struct {D, +, \circ}$ . Then

Preamble

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

Formal statement

theorem Principal_Ideals_in_Integral_Domain {D : Type _} [CommRing D] [IsDomain D] (a b : D) : Ideal.span ({a} : Set D) = Ideal.span ({b} : Set D) ↔ Associated a b := by sorry

Source

https://proofwiki.org/wiki/Principal_Ideals_in_Integral_Domain

View graph