Theorem IsCyclic.normalizer_le_centralizer

Modification history

2026-03-23 08:24
Mathlib/GroupTheory/Transfer.lean
feat(Algebra/Group/Subgroup/Defs): merge `setNormalizer` into `normalizer` (#36852) …
Modified IsCyclic.normalizer_le_centralizerView on Github →
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 →