Revision #2081 → #2623 · back to history
modifiedSymmetric groupc211872a91f5
| Field | From #2081 | To #2623 |
|---|
| mathlib.decl | Equiv.permGroup | Equiv.Perm.permGroup |
| provenance | ai | ai-moderated |
modifiedSymmetric group structure1b66c38c1b2b
| Field | From #2081 | To #2623 |
|---|
| mathlib.decl | Equiv.permGroup | Equiv.Perm.permGroup |
| provenance | ai | ai-moderated |
modifiedInverse via reversing cyclesc9e33d40509b
| Field | From #2081 | To #2623 |
|---|
| mathlib.decl | Equiv.Perm.formPerm_reverse | Cycle.formPerm_reverse |
| provenance | ai | ai-moderated |
modifiedComposition satisfies group axioms55f62e501a65
| Field | From #2081 | To #2623 |
|---|
| mathlib.decl | Equiv.permGroup | Equiv.Perm.permGroup |
| provenance | ai | ai-moderated |
modifiedInverse matrix convention78d23169e0b5
| Field | From #2081 | To #2623 |
|---|
| mathlib.decl | Equiv.Perm.transpose_permMatrix | Matrix.transpose_permMatrix |
| provenance | ai | ai-moderated |