Example 1: $\mathbb{Q}(\sqrt2,\sqrt3)$ has Klein four Galois group and five intermediate fields

Proved

GaloisFundamental.example_sqrt2_sqrt3

by Lucas · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

examplesfield-theorygalois-theory

Let $K = \mathbb{Q}(\sqrt2, \sqrt3) \subseteq \mathbb{R}$ . Then

$[K : \mathbb{Q}] = 4$ ;
$K/\mathbb{Q}$ is Galois;
$\operatorname{Gal}(K/\mathbb{Q})$ is a Klein four-group;
$\operatorname{Gal}(K/\mathbb{Q})$ has exactly $5$ subgroups, and $K/\mathbb{Q}$ has exactly $5$ intermediate fields.

Preamble

import Mathlib

Formal statement

namespace GaloisFundamental

theorem example_sqrt2_sqrt3 :
    Module.finrank ℚ (IntermediateField.adjoin ℚ ({√2, √3} : Set ℝ)) = 4 ∧
      IsGalois ℚ (IntermediateField.adjoin ℚ ({√2, √3} : Set ℝ)) ∧
      IsKleinFour (IntermediateField.adjoin ℚ ({√2, √3} : Set ℝ) ≃ₐ[ℚ]
        IntermediateField.adjoin ℚ ({√2, √3} : Set ℝ)) ∧
      Nat.card (Subgroup (IntermediateField.adjoin ℚ ({√2, √3} : Set ℝ) ≃ₐ[ℚ]
        IntermediateField.adjoin ℚ ({√2, √3} : Set ℝ))) = 5 ∧
      Nat.card (IntermediateField ℚ (IntermediateField.adjoin ℚ ({√2, √3} : Set ℝ))) = 5 := by
  sorry

end GaloisFundamental

Source

Wikipedia, "Fundamental theorem of Galois theory", revision oldid=1345286594, https://en.wikipedia.org/w/index.php?title=Fundamental_theorem_of_Galois_theory&oldid=1345286594, section "Example 1" (Galois group of Q(√2, √3) is the Klein four-group; its five subgroups correspond to the five intermediate fields)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statement, with full knowledge of the source and of the intended meaning. It is not the blind, independent auditor read-back the platform recommends, and no reviewer should treat it as independent evidence of faithfulness. Please compare the Lean code against the source yourself (or regenerate this read-back with an independent auditor) before confirming this item.

Objects. $\sqrt2$ and $\sqrt3$ denote the (non-negative) real square roots. $K$ is the smallest subfield of $\mathbb{R}$ containing $\mathbb{Q}$ , $\sqrt2$ and $\sqrt3$ (the intermediate field of $\mathbb{R}/\mathbb{Q}$ generated by $\{\sqrt2, \sqrt3\}$ ), regarded as a field extension of $\mathbb{Q}$ . $\Gamma$ is the group of $\mathbb{Q}$ -algebra automorphisms of $K$ .

Assertion. All five of the following hold:

$\dim_{\mathbb{Q}} K = 4$ (Mathlib finrank; it would be $0$ if $K$ were infinite-dimensional, so this also asserts finite dimension);
$K/\mathbb{Q}$ is Galois (separable and normal);
$\Gamma$ is a Klein four-group: $|\Gamma| = 4$ and every element $g$ satisfies $g^2 = 1$ (Mathlib's IsKleinFour: cardinality $4$ and exponent $2$ );
the set of all subgroups of $\Gamma$ has exactly $5$ elements;
the set of all intermediate fields of $K/\mathbb{Q}$ (subfields of $K$ , necessarily containing $\mathbb{Q}$ ) has exactly $5$ elements (Mathlib Nat.card, which would be $0$ for an infinite set, so this also asserts finiteness).

Human review

Endorsed by Shuze Chen · Sep 28, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 28, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Example 1: Q(2,3)\mathbb{Q}(\sqrt2,\sqrt3)Q(2​,3​) has Klein four Galois group and five intermediate fields

Example 1: $\mathbb{Q}(\sqrt2,\sqrt3)$ has Klein four Galois group and five intermediate fields