Commit 2024-08-09 08:00 a528f200

feat(GroupTheory/GroupExtension/Defs): define group extensions (#15049) Mainly defines:

• structure GroupExtension N E G: group extensions as short exact sequences 1 → N → E → G → 1
• structure GroupExtension.Equiv S S': equivalences of two group extensions S : GroupExtension N E G and S' : GroupExtension N E' G
• structure GroupExtension.Splitting S: splittings of a group extension S
• def SemidirectProduct.toGroupExtension (φ : G →* MulAut N): the group extension associated with the semidirect product, 1 → N → N ⋊[φ] G → G → 1