Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-17
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.

Distinct normal Sylow subgroups centralize one another

Statement

Normal Sylow subgroups for distinct primes centralize one another. See Sylow p-subgroups of a finite group.

Facts & Assumptions

Given: The hypotheses and objects in the Statement.

[L1]

Let G be a finite group, let p be prime, and write ∣G∣=pam with a∈N and p∤m. A subgroup P≤G is a Sylow p-subgroup when ∣P∣=pa. Equivalently, its order is the largest power of p dividing ∣G∣. This is a property of a subgroup and does not presume that such a subgroup exists; existence is proved in thm-sylow-first-theorem. (Sylow p-subgroups of a finite group).

[L2]

For subgroups A,B≤G, their subgroup commutator is [A,B]=⟨[a,b]:a∈A, b∈B⟩, where [a,b]=aba−1b−1 (def-commutator-and-commutator-subgroup, def-generated-subgroup). The lower central series is γ1(G)=G,γr+1(G)=[G,γr(G)](r≥1). Each γr(G) is characteristic in G, and the series descends because [G,N]≤N whenever N⊴G. (Subgroup commutators and the lower central series).

[L3]

Let G be a group and let N≤G be a subgroup (def-subgroup). For g∈G, write gNg−1:={gng−1:n∈N}. The subgroup N is normal in G when gNg−1=Nfor every g∈G. In that case write N⊴G. Equivalently, every inner conjugation of G maps N onto itself. The connection with equality of the left and right cosets of def-coset is proved in thm-normal-subgroup-characterisations. (Normal subgroup: invariance under conjugation).

[L4]

Let G be a finite group and H≤G. Then ∣G∣=[G:H] ∣H∣. Consequently, under the canonical embedding ι:N→Z, ∣H∣ divides ∣G∣. (Lagrange's theorem: ∣G∣=[G:H]∣H∣ for every subgroup H of a finite group G).

Proof

technique · direct
1.1L1L2L3L4givenalgebra

For normal Sylow p- and q-subgroups with p≠q, every commutator lies in their intersection.

2.1step 1.1givenalgebra∎

Lagrange makes that intersection trivial because its order divides coprime prime powers. This proves the stated claim.

Depends on

Used by

Dependency tree · two levels

20 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