Commit 2024-11-13 20:45 2b629ee8

View on Github →

feat(GroupTheory/Sylow): Surjective group homomorphisms map Sylow subgroups to Sylow subgroups (#18783) This PR shows that surjective group homomorphisms map Sylow subgroups to Sylow subgroups, and that every Sylow subgroup of the codomain arises in this way.

Estimated changes

Modified Mathlib/GroupTheory/Index.lean

added theorem Subgroup.index_map_of_injective

added theorem Subgroup.index_map_subtype

Modified Mathlib/GroupTheory/Sylow.lean

added theorem Sylow.coe_mapSurjective

added def Sylow.mapSurjective

added theorem Sylow.mapSurjective_surjective