Every fractional ideal of Q is principal

Proved

Rat.fractionalIdeal_isPrincipal

by xuanji · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

class-field-theorynumber-theory

Every nonzero fractional ideal of $\mathcal O_{\mathbb Q}$ is principal. Via $\mathcal O_{\mathbb Q}\cong\mathbb Z$ , this is the principal ideal property of the integers, now stated in the fractional-ideal type used by the narrow ray class group. It supplies the principal generator needed to compare ideals with residue classes modulo a rational modulus.

Preamble

import Mathlib.NumberTheory.NumberField.ClassNumber
import Mathlib.RingTheory.ClassGroup.Basic

open NumberField nonZeroDivisors

Formal statement

theorem Rat.fractionalIdeal_isPrincipal
    (I : (FractionalIdeal ((NumberField.RingOfIntegers ℚ)⁰) ℚ)ˣ) :
    ((I : FractionalIdeal ((NumberField.RingOfIntegers ℚ)⁰) ℚ) :
      Submodule (NumberField.RingOfIntegers ℚ) ℚ).IsPrincipal := by sorry

Source

Mathlib, RingTheory/ClassGroup/Basic, ClassGroup.mulEquiv, ClassGroup.card_classGroup_eq_one, and ClassGroup.mk_eq_one_iff, https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/ClassGroup/Basic.html ; Mathlib, NumberTheory/NumberField/Basic, Rat.ringOfIntegersEquiv, https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/NumberField/Basic.html .

View graph