feat(GroupTheory/Focal): add focal subgroup theorem

[Rogerhu12]

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.

---

[github-actions]

PR summary eb5df47f87

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.GroupTheory.Focal (new file)	1150

---

Declarations diff

+ commutator_le_focalSubgroup
+ commutator_le_focalSubgroupOf
+ focalSubgroup
+ focalSubgroupOf
+ focalSubgroupOf_def
+ focalSubgroupOf_eq_closure
+ focalSubgroupOf_mk'_conj_eq
+ focalSubgroup_def
+ focalSubgroup_le
+ focalSubgroup_le_commutator
+ index_eq_sum_minimalPeriod
+ inf_commutator_eq_focalSubgroup
+ inf_ker_transferFocal_eq_focalSubgroup
+ instance : IsMulCommutative (H ⧸ focalSubgroupOf H)
+ instance : Normal (focalSubgroupOf H) := by
+ ker_restrict_transferFocal_eq_focalSubgroupOf
+ map_focalSubgroupOf
+ pow_n_surjective_on_p_quotient
+ quotientKerIsoQuotientFocal
+ transferFocal
+ transfer_focal_eq_pow
+ transfer_restrict_surjective

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[wwylele]

If this is a complete formalization, you can update 1000.yaml

[Rogerhu12]

If this is a complete formalization, you can update 1000.yaml

Thanks for the review and for pointing this out! I wasn't aware of the 1000.yaml file. I've just pushed the update.

[Rogerhu12]

I refactored the development to better match mathlib style.
In particular, I extracted commutator_le_focalSubgroupOf and rewrote commutativity of H ⧸ H* via Normal.quotient_commutative_iff_commutator_le.
I introduced focalSubgroupOf_mk'conj_eq to handle conjugation in the quotient and reused it in the transfer computation.
The commutator-to-kernel step is now inf_le_inf_left _ (Abelianization.commutator_subset_ker ...).
I kept the fusion-style generators in the definition and added focal_gen_eq_commutator as a bridge.
Added @[to_additive] to the core definitions/basic lemmas only.

[tb65536]

Getting close! Just some golfs now, and then we'll need to clean up the names next time around.