TheoremStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13

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.

The Zassenhaus butterfly lemma

Statement

Let $A ⊴ A^{*}$ and $B ⊴ B^{*}$ be subgroups of a group $G$ . Put $X = A (A^{*} \cap B), X^{*} = A (A^{*} \cap B^{*}), Y = (A \cap B^{*}) B, Y^{*} = (A^{*} \cap B^{*}) B .$ Then $X ⊴ X^{*}$ , $Y ⊴ Y^{*}$ , and $X^{*} / X ≅ Y^{*} / Y .$

Facts & Assumptions

Given: Subgroups $A ⊴ A^{*}$ and $B ⊴ B^{*}$ of $G$ , with $X, X^{*}, Y, Y^{*}$ as in the statement.

[L1]

If $H, K, L$ are subgroups with $H \leq L$ and $H K$ a subgroup, then $H (K \cap L) = H K \cap L$ (Dedekind's modular law for subgroup products).

[L2]

If $N ⊴ H$ and $K \leq H$ , then $K N / N ≅ K / (K \cap N)$ ; equivalently, $(K N) / N$ is isomorphic to $K / (K \cap N)$ (Second isomorphism theorem for groups: $H / (H \cap N) ≅ H N / N$ ).

Proof

technique · direct

1.1

Put $M = A^{*} \cap B^{*}$ , $U = A \cap B^{*}$ , and $V = A^{*} \cap B$ . Conjugation by elements of $M$ preserves $U$ and $V$ , because it preserves $A, A^{*}, B, B^{*}$ ; hence $U, V ⊴ M$ and $D : = U V ⊴ M$ .

givenalgebra

2.1

The subgroups $X = A V$ and $X^{*} = A M$ are well defined. The subgroup $M$ normalizes both $A$ and $V$ . Also, for $a \in A$ and $v \in V$ , one has $a v a^{- 1} = (a v a^{- 1} v^{- 1}) v \in A V$ because $A ⊴ A^{*}$ ; hence $A$ normalizes $A V$ and $X ⊴ X^{*}$ . The symmetric argument gives $Y = U B ⊴ M B = Y^{*}$ .

step 1.1algebra

3.1

Apply [L2] inside $X^{*} = A M$ with normal subgroup $X = A V$ : since $X^{*} = X M$ , one has $X^{*} / X ≅ M / (M \cap X)$ .

step 2.1L2

3.2

Symmetrically, [L2] inside $Y^{*} = M B$ with normal subgroup $Y = U B$ gives $Y^{*} / Y ≅ M / (M \cap Y)$ , and [L1] gives $M \cap U B = U (M \cap B) = U V = D$ .

step 1.1step 2.1L1L2

4.1

By [L1], $M \cap A V = (M \cap A) V = U V = D$ , so $X^{*} / X ≅ M / D$ .

step 1.1step 3.1L1

5.1

Both quotients are isomorphic to $M / D$ , so $X^{*} / X ≅ Y^{*} / Y$ ; step 2.1 supplies the two normality assertions.

step 4.1step 3.2∎

Depends on

Used by

The Schreier refinement theorem Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 25 results over 13 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

J. S. Milne, Group Theory, Chapter 6 (standard reference, not scraped)
K. Conrad, Subgroup Series I (standard reference, not scraped)
K. Igusa, Notes on Jordan-Hölder, section 5 (standard reference, not scraped)