Quadratic fields and integer rings

Gaussian, Eisenstein and ℤ[√d] integers, prime factorization there, imaginary quadratic discriminants, class numbers, Stark–Heegner.

• Class number congruences for imaginary quadratic fields
• Imaginary quadratic discriminants
• Norms in imaginary quadratic integer rings
• Gaussian primes
• Schatunowsky-type theorems
• The ring ℤ[√−2]

TheoremStark–Heegner theorem#●ready to prove

Let \(d\) be a positive squarefree integer and let \(K\) be a number field of degree \(2\) over \(\mathbb{Q}\) that contains an element \(x\) with \(x^2 = -d\), so that \(K = \mathbb{Q}(\sqrt{-d})\). Then \(K\) has class number \(1\) if and only if \(d \in \{1, 2, 3, 7, 11, 19, 43, 67, 163\}\).

theorem_wanted stark_heegner_theorem (d : ℕ) (hd_pos : 0 < d) (hd_sf : Squarefree d)
    (K : Type*) [Field K] [NumberField K]
    (hdeg : Module.finrank ℚ K = 2)
    (hsqrt : ∃ x : K, x ^ 2 = algebraMap ℚ K (-(d : ℚ))) :
    NumberField.classNumber K = 1 ↔
    d ∈ ({1, 2, 3, 7, 11, 19, 43, 67, 163} : Finset ℕ)

Sources

• K. Heegner, Diophantische Analysis und Modulfunktionen, Mathematische Zeitschrift 56 (1952), 227–253; A. Baker, Linear forms in the logarithms of algebraic numbers, Mathematika 13–15 (1966–1968); H. M. Stark, A complete determination of the complex quadratic fields of class-number one, Michigan Mathematical Journal 14 (1967), 1–27; see also https://en.wikipedia.org/wiki/Stark%E2%80%93Heegner_theorem.

TheoremUnits of the ring generated by the golden ratio#✓fully proved

Let \(\alpha = (1 + \sqrt{5})/2\) and let \(\mathbb{Z}[\alpha]\) be the subring of \(\mathbb{R}\) generated by \(\alpha\). A real number is a unit of \(\mathbb{Z}[\alpha]\) if and only if it equals \(\alpha^n\) or \(-\alpha^n\) for some integer \(n\).

theorem golden_ratio_integer_ring_units :
    let α : ℝ := (1 + Real.sqrt 5) / 2
    let R := Algebra.adjoin ℤ ({α} : Set ℝ)
    Set.range (fun u : Rˣ => ((u : R) : ℝ)) =
      {x : ℝ | ∃ n : ℤ, x = α ^ n ∨ x = -(α ^ n)}

Sources

• Bahar Demirtürk and Refik Keskin, "Integer Solutions of Some Diophantine Equations via Fibonacci and Lucas Numbers," Journal of Integer Sequences 12 (2009), Article 09.8.7, Theorem 1.1, lines 160–167, https://cs.uwaterloo.ca/journals/JIS/VOL12/Demirturk/demirturk3.tex

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.