Alphabeta MathHow 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.
is a group and
Statement
For every field extension , composition makes a group. If is finite, then
In particular the relative automorphism group is finite.
Facts & Assumptions
Given: A field extension ; for the inequalities, a finite extension, an algebraic closure of , and the Axiom of Choice used by the embedding-extension theorem.
An -automorphism of is an -isomorphism (Relative field automorphisms and ).
Assuming the Axiom of Choice, an embedding extends across the algebraic extension to an -embedding (Assuming Choice, a base-field embedding extends across every algebraic extension); the separable degree is the number of -embeddings (The separable degree as a count of embeddings into an algebraic closure).
For every finite field extension , one has (For a finite extension, ).
Proof
The identity map is an -automorphism, the composite of two -automorphisms is an -automorphism, and the inverse of an -isomorphism is again an -isomorphism fixing ; associativity is inherited from composition. Thus is a group. Every such map fixes and , so no zero case is excluded.
For finite , choose as in [A1]. The map sends into the set of -embeddings and is injective, because and injectivity of imply .
Step 1.2 and the definition of separable degree give , while [L1] gives . If , all three numbers are , so this includes the degree-one endpoint.