TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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.

Dedekind's linear independence theorem for distinct characters

Statement

Let $G$ be a group and $K$ a field. Every finite family of distinct group homomorphisms $G \to K^{\times}$ is linearly independent over $K$ as a family of functions.

Facts & Assumptions

Given: A finite family of pairwise distinct characters $χ_{i} : G \to K^{\times}$ , where character means group homomorphism (Monoid homomorphism and group homomorphism), and linear independence has the function-space meaning of Linear independence: a finite list $v : n \to V$ is independent when $\sum_{i < n} λ_{i} v_{i} = 0_{V}$ forces every $λ_{i} = 0_{F}$ , and a subset $S \subseteq V$ is independent when every injective finite list into $S$ is independent.

[A1]

For every character $χ$ , one has $χ (g x) = χ (g) χ (x)$ , and every value $χ (g)$ lies in $K^{\times}$ and is nonzero.

Proof

technique · contradiction

1.1

The empty family is independent vacuously, and a singleton is independent because its character never vanishes. Suppose, for contradiction, that some finite distinct family is dependent; among all nonzero relations choose one with the least support, relabel its supported characters as $χ_{1}, \dots, χ_{r}$ , and divide by the first nonzero coefficient to write $\sum_{i = 1}^{r} a_{i} χ_{i} (x) = 0$ for every $x \in G$ , where $r \geq 2$ and $a_{1} = 1$ .

assume-contrachoose

2.1

Since $χ_{1} \neq χ_{r}$ , choose $g \in G$ with $χ_{1} (g) \neq χ_{r} (g)$ . Evaluate the relation of step 1.1 at $g x$ and subtract $χ_{r} (g)$ times its value at $x$ to obtain $\sum_{i = 1}^{r - 1} a_{i} (χ_{i} (g) - χ_{r} (g)) χ_{i} (x) = 0$ for every $x \in G$ .

step 1.1A1choosealgebra

3.1

The new relation has support smaller than $r$ but is nonzero because its $χ_{1}$ -coefficient is $χ_{1} (g) - χ_{r} (g) \neq 0$ . This contradicts the minimality in step 1.1, so no nontrivial relation exists and the characters are linearly independent.

step 1.1step 2.1discharge-contradiction∎

Depends on

Used by

Artin's fixed-field lower bound [K:K^G]≥ |G| Lemma

Dependency tree · two levels

14 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, Theorem 5.14 (standard reference, not scraped)