LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-27

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.

A quadratic extension in characteristic not $2$ is obtained by adjoining a square root

Statement

Let $E / F$ be a field extension with $[E : F] = 2$ and $char F \neq 2$ . Then there is $d \in F$ such that $E = F (\sqrt{d})$ . In fact $d$ may be chosen to be a nonsquare in $F$ .

Facts & Assumptions

Given: A quadratic extension $E / F$ with $char F \neq 2$ .

[L1]

An algebraic element has a unique monic irreducible minimal polynomial, and its degree equals the degree of the corresponding simple extension (The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element, A simple algebraic extension is its minimal-polynomial quotient and has power basis $1, a, \dots, a^{n - 1}$ and degree $n$ ).

[L2]

In a finite tower of fields, degrees multiply (Tower law for finite extensions: $[L : F] = [L : K] [K : F]$ ).

Proof

technique · direct

1.1

Choose $α \in E ∖ F$ . Then $F ⊊ F (α) \subseteq E$ . Since $[E : F] = 2$ , fact [L2] forces $[F (α) : F] = 2$ and hence $E = F (α)$ . Therefore [L1] gives $m_{α} (x) = x^{2} + b x + c$ with $b, c \in F$ .

L1L2choose

2.1

Because $char F \neq 2$ , the element $2$ is invertible in $F$ . Put $δ : = 2 α + b .$ Using $m_{α} (α) = 0$ , $δ^{2} = 4 α^{2} + 4 b α + b^{2} = b^{2} - 4 c \in F .$

step 1.1algebra

3.1

Also $α = \frac{δ - b}{2},$ so $F (α) = F (δ)$ . Therefore $E = F (α) = F (δ) = F (\sqrt{d})$ with $d : = δ^{2} \in F$ . If $d$ were already a square in $F$ , then $δ \in F$ and the displayed formula would give $α \in F$ , contradicting step 1.1. Hence $d$ may be chosen nonsquare.

step 2.1step 1.1algebra∎

Depends on

Used by

The complex numbers are algebraically closed Theorem

Dependency tree · two levels

12 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

J. S. Milne, Fields and Galois Theory, v5.10, Lemma 3.25 (standard reference, not scraped)

A quadratic extension in characteristic not 22 is obtained by adjoining a square root