Commit 2025-08-29 14:13 e29fe6f8

View on Github →

feat: Group isomorphisms between (Equiv.Perm|alternatingGroup)s (#27498) Required to prove that A_n is simple iff n = 3 or 5 ≤ n(#26051).

Estimated changes

Modified Mathlib/Algebra/Group/End.lean

deleted def Equiv.Perm.permCongrHom

deleted theorem Equiv.Perm.permCongr_eq_mul

added def Equiv.permCongrHom

added theorem Equiv.permCongrHom_coe

added theorem Equiv.permCongrHom_coe_equiv

added theorem Equiv.permCongrHom_symm

added theorem Equiv.permCongrHom_trans

added theorem Equiv.permCongr_eq_mul

added theorem Equiv.permCongr_mul

Modified Mathlib/GroupTheory/RegularWreathProduct.lean

Modified Mathlib/GroupTheory/SpecificGroups/Alternating.lean

added def Equiv.altCongrHom