Revision #1610 → #2652 · back to history
modifiedCycle taken to k-th power13f8990b332b
| Field | From #1610 | To #2652 |
|---|
| mathlib.decl | Equiv.Perm.IsCycle.isCycle_pow_iff | Equiv.Perm.IsCycle.pow_iff |
| provenance | ai | ai-moderated |
modifiedA_n normal of index 26306c32a9e72
| Field | From #1610 | To #2652 |
|---|
| mathlib.decl | Equiv.Perm.alternatingGroup.index_eq_two | alternatingGroup.index_eq_two |
| provenance | ai | ai-moderated |
modifiedKlein four-group in S_402124033c376
| Field | From #1610 | To #2652 |
|---|
| mathlib.decl | Equiv.Perm.alternatingGroup.kleinFour | alternatingGroup.kleinFour |
| provenance | ai | ai-moderated |
modifiedA_n simple for n ≥ 50311767a9aa8
| Field | From #1610 | To #2652 |
|---|
| mathlib.decl | Equiv.Perm.alternatingGroup.isSimpleGroup | alternatingGroup.isSimpleGroup |
| provenance | ai | ai-moderated |
modifiedNormal subgroups of finite S_n7e135d394b9b
| Field | From #1610 | To #2652 |
|---|
| mathlib.decl | Equiv.Perm.alternatingGroup.normal | alternatingGroup.normal |
| provenance | ai | ai-moderated |