LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-27

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.

Frobenius kernel cardinality

Statement

Let $G$ be a finite Frobenius group with complement $H$ and let $N = (G ∖ ⋃_{x \in G} x H x^{- 1}) \cup {1}$ be its kernel set. Then

$∣ N ∣ = [G : H], N \cap H = {1} .$

Facts & Assumptions

Given: A finite group $G$ , a Frobenius complement ${1} < H < G$ , and the kernel set $N = (G ∖ ⋃_{x \in G} x H x^{- 1}) \cup {1}$ .

[F1]

An element $g$ lies in $N$ exactly when $g = 1$ or $g \notin x H x^{- 1}$ for every $x \in G$ (Frobenius kernel set).

[F2]

$H \cap g H g^{- 1} = {1}$ for every $g \notin H$ , and ${1} < H < G$ (Frobenius complement and frobenius group).

[F3]

$N_{G} (H) = {g \in G : g H g^{- 1} = H}$ is a subgroup of $G$ containing $H$ (The normalizer $N_{G} (H) = {g \in G : g H g^{- 1} = H}$ of a subgroup, $C_{G} (x)$ and $N_{G} (H)$ are subgroups of $G$ ).

[F4]

The rule $g N_{G} (H) \mapsto g H g^{- 1}$ is a well-defined bijection $G / N_{G} (H) \to {g H g^{- 1} : g \in G}$ ; for finite $G$ the number of distinct conjugates of $H$ is $[G : N_{G} (H)]$ (The conjugates of $H$ are in bijection with $G / N_{G} (H)$ and, for finite $G$ , number $[G : N_{G} (H)]$ ).

[F5]

For a finite group $G$ and $H \leq G$ one has $∣ G ∣ = [G : H] ∣ H ∣$ (Lagrange's theorem: $∣ G ∣ = [G : H] ∣ H ∣$ for every subgroup $H$ of a finite group $G$ ).

[F6]

$[G : H]$ is the cardinality of the left coset set $G / H$ (The coset set $G / H$ and the index $[G : H]$ of a subgroup).

Proof

technique · direct

1.1

One has $N_{G} (H) = H$ . In one direction $H \subseteq N_{G} (H)$ , since $h H h^{- 1} = H$ for $h \in H$ . Conversely let $g \in N_{G} (H)$ ; then $g H g^{- 1} = H$ and hence $H = H \cap g H g^{- 1}$ . If $g \notin H$ then [F2] makes this intersection ${1}$ , contradicting ${1} < H$ ; so $g \in H$ .

F2F3given

1.2

Nonidentity elements of distinct conjugates do not overlap: if $1 \neq y \in x H x^{- 1} \cap z H z^{- 1}$ for some $x, z \in G$ , then $y = x u x^{- 1} = z v z^{- 1}$ for some $u, v \in H$ , whence $u = x^{- 1} z v z^{- 1} x = (x^{- 1} z) v (x^{- 1} z)^{- 1} \in H \cap s H s^{- 1}$ with $s = x^{- 1} z$ . Since $u \neq 1$ , [F2] forces $s \in H$ , that is $z \in x H$ , and then $z H z^{- 1} = x H x^{- 1}$ .

F2algebra

2.1

Consequently the distinct subgroups of the form $x H x^{- 1}$ are in bijection with the left cosets of $H$ , so there are exactly $[G : H]$ of them: [F4] identifies the set of conjugates with $G / N_{G} (H)$ , and step 1.1 together with [F6] identifies the cardinality of that coset space with $[G : H]$ .

F3F4F6step 1.1

3.1

Every conjugate $x H x^{- 1}$ has exactly $∣ H ∣$ elements, and by step 1.2 each nonidentity element of the union $⋃_{x \in G} x H x^{- 1}$ lies in exactly one of the conjugates; the element $1$ lies in all of them. Hence the union has $1 + [G : H] (∣ H ∣ - 1)$ elements.

step 2.1step 1.2algebra

4.1

Therefore $∣ N ∣ = ∣ G ∣ - (1 + [G : H] (∣ H ∣ - 1)) + 1 = ∣ G ∣ - [G : H] (∣ H ∣ - 1)$ , and Lagrange's identity $∣ G ∣ = [G : H] ∣ H ∣$ of [F5] turns this into $∣ N ∣ = [G : H] ∣ H ∣ - [G : H] ∣ H ∣ + [G : H] = [G : H]$ .

F1F5step 3.1algebra

5.1

Finally $N \cap H = {1}$ : the identity lies in both sets, while a nonidentity element $h \in H$ lies in the conjugate $1 H 1^{- 1} = H$ , so by the description [F1] of $N$ it is not an element of $N$ . ∎

F1given

Depends on

Used by

Frobenius semidirect product decomposition Corollary
Frobenius kernel closure is the content of the theorem Remark

Dependency tree · two levels

24 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

Alex Bartel, Introduction to Representation Theory of Finite Groups, §6.1 (standard reference, not scraped)