Class number problem for real quadratic fields

Reference: Wikipedia

def ClassNumberProblem.IsClassNumberOne (d : ℤ) : Prop

Equations

• ClassNumberProblem.IsClassNumberOne d = ∃ (h₂ : Irreducible (Polynomial.X ^ 2 - Polynomial.C ↑d)), NumberField.classNumber (AdjoinRoot (Polynomial.X ^ 2 - Polynomial.C ↑d)) = 1

theorem ClassNumberProblem.class_number_problem : {d : ℤ | Squarefree d ∧ d > 1 ∧ IsClassNumberOne d}.Infinite

There are infinitely many real quadratic fields ℚ(√d) with class number one, where d > 1 is a squarefree integer.

theorem ClassNumberProblem.class_number_problem.variants.imaginary : {d : ℤ | Squarefree d ∧ d < 0 ∧ IsClassNumberOne d} = {-1, -2, -3, -7, -11, -19, -43, -67, -163}

Stark–Heegner theorem : For any squarefree integer d < 0, the class number of the imaginary quadratic field Q(√d) is one if and only if d ∈ {-1, -2, -3, -7, -11, -19, -43, -67, -163}.