Theorem IsCyclic.normalizer_le_centralizer

Modification history

2024-12-20 19:39
Mathlib/GroupTheory/Transfer.lean
feat(GroupTheory/Transfer): A cyclic Sylow subgroup for the smallest prime has a normal complement (#19587) …
Added IsCyclic.normalizer_le_centralizerView on Github →