Def Equiv.Perm.permCongrHom

Modification history

2025-08-29 14:13
Mathlib/Algebra/Group/End.lean
feat: Group isomorphisms between (`Equiv.Perm`|`alternatingGroup`)s (#27498) …
Deleted Equiv.Perm.permCongrHomView on Github →
2025-06-16 12:56
Mathlib/Algebra/Group/End.lean
feat(GroupTheory): add Regular Wreath Product (#24816) …
Added Equiv.Perm.permCongrHomView on Github →