Revision #2651 → #3196 · back to history
addedLagrange's theoremebfa1d37e038
modifiedSylow Theorem 1 (Existence)68f36ab8bc45
| Field | From #2651 | To #3196 |
|---|
| provenance | ai | ai-moderated |
modifiedSylow subgroups have equal order and are conjugatedce80e8f7b01
| Field | From #2651 | To #3196 |
|---|
| note | `Sylow.isPretransitive_of_finite` says G acts transitively on Sylow p-subgroups; `Sylow.equiv` provides the resulting isomorphism. | `Sylow.isPretransitive_of_finite` says G acts transitively on Sylow p-subgroups, whence the resulting isomorphism. |
addedFrattini's argumentef27a56ae5cd
addedFocal subgroup theoremfcb5ed94b23b
addedOrbit-stabilizer theorem (used in proof)182a938e7f55