TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

Norm is multiplicative, trace is $F$ -linear, and both are transitive in towers

Statement

Let $K / F$ be a finite extension and let $a, b \in K$ .

$N_{K / F} (a b) = N_{K / F} (a) N_{K / F} (b)$ .
${Tr}_{K / F} (a + b) = {Tr}_{K / F} (a) + {Tr}_{K / F} (b)$ and ${Tr}_{K / F} (c a) = c {Tr}_{K / F} (a)$ for every $c \in F$ .
If $L / K / F$ is a tower of finite extensions, then $N_{L / F} = N_{K / F} \circ N_{L / K}, {Tr}_{L / F} = {Tr}_{K / F} \circ {Tr}_{L / K} .$

Facts & Assumptions

Given: Finite field extensions as in the Statement, multiplication maps $m_{x}$ for $x \in K$ or $x \in L$ , and product bases in towers.

[F1]

Norm and trace are the determinant and trace of multiplication-by- $x$ on the relevant finite-dimensional vector space (The norm $N_{K / F}$ and trace ${Tr}_{K / F}$ of a finite field extension, The determinant of an endomorphism of a finite-dimensional vector space: its matrix determinant in an ordered basis in positive dimension, and $1$ on the zero space, The basis-independent trace of an endomorphism of a finite-dimensional vector space).

[L1]

For same-sized square matrices over a commutative ring, determinant is multiplicative (For same-sized finite square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$ ).

[L2]

The embedding formulas identify norm with the product and trace with the sum of the conjugates, counted with the inseparable exponent (Norm and trace from embeddings, with the inseparable exponent in the norm formula).

[L3]

In a finite tower, a basis of the top field over the middle field times a basis of the middle field over the base is a basis of the top field over the base (Products of bases form a basis in a tower of finite extensions, Tower law for finite extensions: $[L : F] = [L : K] [K : F]$ ).

[L4]

Restriction from the $F$ -embeddings of $L$ to the $F$ -embeddings of $K$ is surjective, and every fibre has cardinality $[L : K]_{s}$ after transporting the $K$ -structure (Restriction partitions embeddings in a finite tower into extension fibres).

[L5]

Separable degrees multiply in finite towers: $[L : F]_{s} = [L : K]_{s} [K : F]_{s}$ (Separable degree is multiplicative in finite towers: $[L : F]_{s} = [L : K]_{s} [K : F]_{s}$ ).

Proof

technique · direct

1.1

Multiplication operators compose as $m_{a b} = m_{a} \circ m_{b}$ , because $(m_{a} \circ m_{b}) (x) = a (b x) = (a b) x$ . Therefore [F1] and [L1] give $N_{K / F} (a b) = \det (m_{a b}) = \det (m_{a}) \det (m_{b}) = N_{K / F} (a) N_{K / F} (b) .$

F1L1algebra

1.2

The operator identity $m_{a + b} = m_{a} + m_{b}$ and the scalar identity $m_{c a} = c m_{a}$ make trace additive and $F$ -linear. Hence [F1] gives ${Tr}_{K / F} (a + b) = {Tr}_{K / F} (a) + {Tr}_{K / F} (b), {Tr}_{K / F} (c a) = c {Tr}_{K / F} (a) .$

F1algebra

1.3

Let $L / K / F$ be a finite tower, fix an algebraic closure $Ω / F$ , and write $i_{L / F}$ , $i_{L / K}$ , and $i_{K / F}$ for the three inseparable degrees. For an $F$ -embedding $σ : K \to Ω$ , let $E_{σ}$ be its restriction fibre in ${Hom}_{F} (L, Ω)$ . Applying the embedding formulas [L2] to $L / K$ after transporting scalars along $σ$ gives $σ (N_{L / K} (a)) = {(\prod_{τ \in E_{σ}} τ (a))}^{i_{L / K}}, σ ({Tr}_{L / K} (a)) = i_{L / K} \sum_{τ \in E_{σ}} τ (a) .$ The fibres $E_{σ}$ partition ${Hom}_{F} (L, Ω)$ by [L4].

L2L4

1.4

By the ordinary tower law [L3] and separable-degree multiplicativity [L5], $i_{L / F} = \frac{[L : F]}{[L : F]_{s}} = \frac{[L : K] [K : F]}{[L : K]_{s} [K : F]_{s}} = i_{L / K} i_{K / F} .$

L3L5algebra

2.1

Apply the outer embedding formulas [L2] for $K / F$ to the two elements in step 1.3. Using the fibre partition and step 1.4 gives $N_{K / F} (N_{L / K} (a)) = {(\prod_{σ} \prod_{τ \in E_{σ}} τ (a)^{i_{L / K}})}^{i_{K / F}} = {(\prod_{τ \in {Hom}_{F} (L, Ω)} τ (a))}^{i_{L / F}} = N_{L / F} (a),$ and similarly ${Tr}_{K / F} ({Tr}_{L / K} (a)) = i_{K / F} i_{L / K} \sum_{τ \in {Hom}_{F} (L, Ω)} τ (a) = {Tr}_{L / F} (a) .$

L2step 1.3step 1.4algebra

3.1

Steps 1.1, 1.2, and 2.1 prove the three claims.

step 1.1step 1.2step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

33 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, Proposition 5.48 (standard reference, not scraped)
B. Conrad, Norm and trace, Theorem 3.2 (standard reference, not scraped)

Norm is multiplicative, trace is FF-linear, and both are transitive in towers