Theorems · Definition · group theory

SemidirectProduct.rightHom

{N : Type u_1} → {G : Type u_2} → [inst : Group N] → [inst_1 : Group G] → {φ : G →* MulAut N} → N ⋊[φ] G →* G

The canonical projection map N ⋊[φ] G →* G, as a group hom.

Defined in

Mathlib.GroupTheory.SemidirectProduct

Cited by

9 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext, Quot.sound

Assumes

GroupGroup