LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-26

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

For $E / F$ finite Galois and $L / F$ finite inside a common field, $[E L : F] = [E : F] [L : F] / [E \cap L : F]$

Statement

Let $E / F$ be a finite Galois extension (Finite Galois extensions and $Gal (K / F)$ ) and $L / F$ a finite extension (The degree $[K : F] = \dim_{F} K$ of a finite field extension), both subfields of a common field. Then the compositum $E L$ is finite over $F$ and

$[E L : F] = \frac{[E : F] [L : F]}{[E \cap L : F]} .$

Only one of the two extensions is required to be Galois.

Facts & Assumptions

Given: Subfields $E$ and $L$ of a common field, both containing $F$ , with $E / F$ finite Galois and $L / F$ finite; $E \cap L$ is a subfield containing $F$ and contained in $E$ , hence an intermediate field of $E / F$ .

[L1]

For $E / F$ finite Galois and $L / F$ an extension inside a common overfield, $E L / L$ is finite Galois and restriction gives $Gal (E L / L) ≅ Gal (E / E \cap L)$ (The Galois translation theorem).

[L2]

If $K / F$ is finite Galois and $F \subseteq E^{'} \subseteq K$ , then $K / E^{'}$ is finite Galois (A finite Galois extension is Galois over every intermediate field).

[L3]

For fields $F \subseteq K \subseteq M$ with $K / F$ and $M / K$ finite, $M / F$ is finite and $[M : F] = [M : K] [K : F]$ (Tower law for finite extensions: $[L : F] = [L : K] [K : F]$ ).

[L4]

For finite subextensions $E / F$ and $E^{'} / F$ of a common field, the compositum is finite and $[E E^{'} : F] \leq [E : F] [E^{'} : F]$ (For finite subextensions in a common field, $[E E^{'} : F] \leq [E : F] [E^{'} : F]$ ).

[L5]

For a finite Galois extension $M / K$ one has $∣ Gal (M / K) ∣ = [M : K]$ (Equivalent characterizations of a finite Galois extension).

Proof

technique · direct

1.1L2given

$E \cap L$ is an intermediate field of $E / F$ , so $E / (E \cap L)$ is finite Galois by [L2].

1.2L4given

By [L4] the compositum $E L$ is finite over $F$ .

1.3L3given

Applying [L3] to $F \subseteq E \cap L \subseteq E$ gives $[E : F] = [E : E \cap L] [E \cap L : F]$ , so $[E : E \cap L] = [E : F] / [E \cap L : F]$ .

2.1step 1.1step 1.2L1L5

By [L1] the extension $E L / L$ is finite Galois with $Gal (E L / L) ≅ Gal (E / E \cap L)$ , so [L5] applied to both sides gives $[E L : L] = ∣ Gal (E L / L) ∣ = ∣ Gal (E / E \cap L) ∣ = [E : E \cap L]$ .

3.1step 2.1step 1.3L3∎

Applying [L3] to $F \subseteq L \subseteq E L$ and substituting steps 2.1 and 1.3 gives $[E L : F] = [E L : L] [L : F] = [E : E \cap L] [L : F] = [E : F] [L : F] / [E \cap L : F]$ .

Remarks

The Galois hypothesis is not decoration. Without it the formula fails: over $F = Q$ take $E = Q (\sqrt[3]{2})$ and $L = Q (ω \sqrt[3]{2})$ inside a splitting field of $t^{3} - 2$ , where $ω$ is a primitive cube root of unity. Both have degree three over $Q$ , since $t^{3} - 2$ is irreducible there. The compositum contains $ω = (ω \sqrt[3]{2}) / \sqrt[3]{2}$ , hence contains the splitting field $Q (\sqrt[3]{2}, ω)$ and equals it, so $[E L : Q] = 6$ . And $E \cap L = Q$ : its degree over $Q$ divides $3$ by the tower law, and it cannot be $3$ , since $E = E \cap L = L$ would put $ω$ in $E$ and force $[E : Q] \geq 6$ . The formula would predict $9$ . Neither $E$ nor $L$ is Galois over $Q$ .

Depends on

Used by

FALSE: a polynomial solvable by radicals must have abelian Galois group False statement
ℚ(μₘ)∩ℚ(μₙ)=ℚ(μ_gcd(m,n)) Theorem

Dependency tree · two levels

26 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

K. Conrad, Cyclotomic Extensions (expository blurb), Section 3 (standard reference, not scraped)
J. S. Milne, Fields and Galois Theory, v5.10, Chapter 3, composita and translation (standard reference, not scraped)

For E/FE/F finite Galois and L/FL/F finite inside a common field, [EL:F]=[E:F][L:F]/[E∩L:F][EL:F]=[E:F][L:F]/[E∩L:F]