TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-11

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.

Any two finite free bases of the same group have the same cardinality

Statement

If $B$ and $C$ are finite free bases of the same group $F$ , then $∣ B ∣ = ∣ C ∣$ .

Facts & Assumptions

Given: A group $F$ with finite free bases $B$ and $C$ , and the group $C_{2} : = Sym ({0, 1})$ .

[L1]

If $A$ and $B$ are finite, then $A^{B}$ is finite and $∣ A^{B} ∣ = ∣ A ∣^{∣ B ∣}$ (The set $A^{B}$ of functions $B \to A$ between finite sets is finite, with $∣ A^{B} ∣ = ∣ A ∣^{∣ B ∣}$ ).

[L2]

For $m, n \in N$ , the natural number $m^{n}$ and the real number $m^{n}$ agree under the canonical inclusion $N \subseteq R$ (Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $R$ ).

[L3]

If $a > 1$ , then $a^{m} < a^{n}$ whenever $m < n$ in $N$ (Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ ).

[L4]

For naturals $m, n$ , exactly one of $m < n$ , $m = n$ , $m > n$ holds (Trichotomy of the order on $N$ ).

[L5]

$(Sym (X), \circ, {id}_{X})$ is a group for every set $X$ ( $Sym (X)$ is a group under composition, and it is non-abelian whenever $X$ has at least three distinct elements).

[F1]

If $A$ is finite and $f : A \to B$ is a bijection, then $B$ is finite and $∣ B ∣ = ∣ A ∣$ (The cardinality $∣ A ∣$ of a finite set).

Proof

technique · direct

1.1

Every permutation of ${0, 1}$ is determined by the image of $0$ : it is either the identity or the transposition $(0 1)$ , and these two maps are distinct; hence $C_{2}$ is a group with exactly two elements.

L5algebra

2.1

Restriction to $B$ maps $Hom (F, C_{2})$ to the function set $C_{2}^{B}$ , and the free-basis property gives a unique homomorphic extension of every function $B \to C_{2}$ ; restriction and extension are inverse maps, so restriction is a bijection $Hom (F, C_{2}) \to C_{2}^{B}$ ; [L1] counts $∣ C_{2}^{B} ∣ = 2^{∣ B ∣}$ and [F1] transports that count along the bijection, giving $∣ Hom (F, C_{2}) ∣ = 2^{∣ B ∣}$ , including $B = \emptyset$ .

F1L1step 1.1given

3.1

Applying the same restriction-extension bijection to $C$ gives $∣ Hom (F, C_{2}) ∣ = 2^{∣ C ∣}$ , and therefore $2^{∣ B ∣} = 2^{∣ C ∣}$ as natural numbers.

step 2.1given

4.1

If $∣ B ∣ < ∣ C ∣$ , then [L2] lets the equality of step 3.1 be read in $R$ , and [L3] applied to the base $2 > 1$ gives $2^{∣ B ∣} < 2^{∣ C ∣}$ , contradicting step 3.1; the case $∣ C ∣ < ∣ B ∣$ is symmetric, so trichotomy [L4] forces $∣ B ∣ = ∣ C ∣$ .

L2L3L4step 3.1algebra

5.1

Thus any two finite free bases of $F$ , including empty bases, have the same cardinality.

step 4.1∎

Depends on

Used by

The rank of a free group admitting a finite basis Definition
Grushko decomposition and rank additivity Theorem

Dependency tree · two levels

47 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

Richard Elman, Lectures on Abstract Algebra, §18 (standard reference, not scraped)
Encyclopedia of Mathematics, Free group (standard reference, not scraped)