Theorems · Definition · group theory

SemidirectProduct.toGroupExtension

{N : Type u_1} →
  {G : Type u_3} → [inst : Group G] → [inst_1 : Group N] → (φ : G →* MulAut N) → GroupExtension N (N ⋊[φ] G) G

The group extension associated to the semidirect product

Defined in

Mathlib.GroupTheory.GroupExtension.Defs

Cited by

3 results in Mathlib

Foundations

Depth 36 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupGroup