is a fundamental unit of or the square of one
ProvedClassNumberFormula.pellEpsilon_fundamental_unit_or_squareclass-number-formulanumber-theory
Let be a fundamental discriminant and let , presented as a quadratic number field with an element satisfying . Let , be the solution of with minimal and put . Then there is a unit such that
- is a fundamental unit: every unit of equals or for some ;
- or .
Formalization Note A fundamental unit is taken here to be any generator of the unit group modulo , without the normalisation under a real embedding. The choice of square root of replaces by its conjugate , and the statement holds for either choice.
Preamble
import Mathlib import Definitions.Def_ClassNumberFormula_Kronecker import Definitions.Def_ClassNumberFormula_FormClassNumber open NumberField NumberField.InfinitePlace NumberField.Units Filter Topology Real
Formal statement
namespace ClassNumberFormula
theorem pellEpsilon_fundamental_unit_or_square (d : ℤ) (hd : IsFundamentalDiscriminant d)
(hpos : 0 < d) (K : Type*) [Field K] [NumberField K] (hK : Module.finrank ℚ K = 2)
(α : K) (hα : α ^ 2 = (d : K)) :
∃ η : (𝓞 K)ˣ, (∀ v : (𝓞 K)ˣ, ∃ n : ℤ, v = η ^ n ∨ v = -η ^ n) ∧
(((η : 𝓞 K) : K) = ((pellT d : K) + (pellU d : K) * α) / 2 ∨
((η : 𝓞 K) : K) ^ 2 = ((pellT d : K) + (pellU d : K) * α) / 2) := by sorry
end ClassNumberFormulaSource
Wikipedia, "Class number formula" (revision oldid=1366411311), https://en.wikipedia.org/w/index.php?title=Class_number_formula&oldid=1366411311, section "Dirichlet class number formula" ("Then is either a fundamental unit of the real quadratic field or the square of a fundamental unit.")
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.