Theorem IsCyclic.isComplement'

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.isComplement'View on Github →