DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-17

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.

The separable degree $[K : F]_{s}$ as a count of embeddings into an algebraic closure

Definition

Let $K / F$ be a finite field extension (The degree $[K : F] = \dim_{F} K$ of a finite field extension) and let $Ω / F$ be an algebraic closure. Assuming Choice, such a field exists by Assuming Choice, every field has an algebraic closure. The separable degree of $K / F$ is

$[K : F]_{s} : = ∣ {Hom}_{F} (K, Ω) ∣,$

where ${Hom}_{F}$ denotes the set of $F$ -embeddings of $F$ -homomorphisms and $F$ -embeddings of field extensions. This set is finite: a finite $F$ -basis generates $K$ , an embedding is determined by the images of those finitely many generators, and each image is among the finitely many roots of its minimal polynomial by $F$ -embeddings of $F (α)$ into an algebraically closed field correspond to the distinct roots of $m_{α}$ . Thus its cardinality is defined by The cardinality $∣ A ∣$ of a finite set. The value is independent of the chosen algebraic closure by The separable degree is independent of the chosen algebraic closure ↗.

Depends on

Dependency tree · 2 levels

Sources