ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-16

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 a field extension $K / F$ , one has $K \otimes_{F} F^{n} ≅ K^{n}$

Example

For a field extension $K / F$ and a natural number $n$ , there is a canonical $K$ -linear isomorphism

$K \otimes_{F} F^{n} ≅ K^{n},$

given by $k \otimes (a_{0}, \dots, a_{n - 1}) \mapsto (k a_{0}, \dots, k a_{n - 1})$ . The assertion includes $n = 0$ .

Facts & Assumptions

Given: A field extension $K / F$ and a natural number $n$ .

[L1]

The specified embedding $F \to K$ makes $K \otimes_{F} -$ the extension-of-scalars functor (Field extensions, generated subrings $F [S]$ , generated subfields $F (S)$ , and simple extensions, Restriction of scalars and extension of scalars $S \otimes_{R} M$ along a ring homomorphism $R \to S$ ).

[L2]

The coordinate vectors $e_{0}, \dots, e_{n - 1}$ form a basis of $F^{n}$ , with the empty basis when $n = 0$ (The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ ).

[L3]

A prescription $Q (k \otimes a) : = q (k, a)$ extends to a homomorphism on $K \otimes_{F} F^{n}$ if and only if $q$ is balanced, and the extension is then unique (A formula on elementary tensors defines a homomorphism exactly when its underlying pairing is balanced).

Verification

technique · direct

1.1

The pairing $(k, (a_{j})) \mapsto (k a_{j})$ is $F$ -balanced, so [L3] gives a unique additive $T : K \otimes_{F} F^{n} \to K^{n}$ with $T (k \otimes (a_{j})) = (k a_{j})$ , and $T$ is $K$ -linear by [L1]. It sends $1 \otimes e_{j}$ to the $j$ th standard coordinate vector.

givenL1L2L3algebra

2.1

Define $S : K^{n} \to K \otimes_{F} F^{n}$ by $S ((k_{j})_{j < n}) = \sum_{j < n} k_{j} \otimes e_{j}$ , which is additive and $K$ -linear by [L1]. Then $T (S ((k_{j}))) = (k_{j})$ because $T (k_{j} \otimes e_{j})$ is $k_{j}$ in coordinate $j$ and zero elsewhere, and on a generator $S (T (k \otimes a)) = \sum_{j < n} k a_{j} \otimes e_{j} = \sum_{j < n} k \otimes a_{j} e_{j} = k \otimes a$ , moving each $F$ -scalar $a_{j}$ across the balanced tensor by [L1] and expanding $a$ in the basis of [L2]. Both composites are additive and agree on generators, so $T$ is an isomorphism.

step 1.1L1L2L3

3.1

At $n = 0$ both modules are zero — the empty sum defining $S$ is $0$ — so the same argument gives the unique isomorphism.

step 2.1L1L2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 89 results over 20 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

MIT 18.721, Introduction to Algebraic Geometry, §2.1 (standard reference, not scraped)
Wenqi Li, Commutative Algebra, Lecture 9 (standard reference, not scraped)

For a field extension K/FK/F, one has K⊗FFn≅KnK⊗F​Fn≅Kn