Revision #1609 → #2651 · back to history
modifiedSubgroup of every prime-power order7ca769abcd55
| Field | From #1609 | To #2651 |
|---|
| mathlib.decl | exists_subgroup_card_pow_prime | Sylow.exists_subgroup_card_pow_prime |
| provenance | ai | ai-moderated |
modifiedp-nilpotency from central Sylow normalizer4e2f7cc57c1c
| Field | From #1609 | To #2651 |
|---|
| mathlib.decl | ker_transferSylow_isComplement' | MonoidHom.ker_transferSylow_isComplement' |
| provenance | ai | ai-moderated |
modifiedTheorem 1 (proof statement)b6efd4feed6c
| Field | From #1609 | To #2651 |
|---|
| mathlib.decl | exists_subgroup_card_pow_prime | Sylow.exists_subgroup_card_pow_prime |
| provenance | ai | ai-moderated |
modifiedConstructive existence of Sylow p-subgroup5b3284b64183
| Field | From #1609 | To #2651 |
|---|
| mathlib.decl | exists_subgroup_card_pow_succ | Sylow.exists_subgroup_card_pow_succ |
| provenance | ai | ai-moderated |