Principal_Ideals_of_Integers

Proved

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

idealsintegersproofwikiring-theory

Let $J$ be a non-zero ideal of $\Z$ . Then $J = \ideal b$ where $b$ is the smallest strictly positive integer belonging to $J$ .

Preamble

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

Formal statement

theorem Principal_Ideals_of_Integers (J : Ideal ℤ) (hJ : J ≠ ⊥) : ∃ b : ℤ, 0 < b ∧ J = Ideal.span {b} := by sorry

Source