Commit 2026-02-26 14:02 90953019

View on Github →

feat(GroupTheory/Focal): add focal subgroup theorem (#34380) Define focalSubgroup (denoted H*) and prove the Focal Subgroup Theorem. The main result is inf_commutator_eq_focalSubgroup, which states that for a Sylow p-subgroup P of a finite group G, P ∩ G' = P*. This implementation includes:

  • The definition of the focal subgroup.
  • The transfer homomorphism G → P/P*.
  • The proof using the transfer map. Also add [gorenstein1968] to docs/references.bib.

Estimated changes

modified theorem Sylow.not_dvd_index