Theorems · Inductive type · group theory

SemidirectProduct

(N : Type u_1) → (G : Type u_2) → [inst : Group N] → [inst_1 : Group G] → (G →* MulAut N) → Type (max u_1 u_2)

The semidirect product of groups N and G, given a map φ from G to the automorphism group of N. It is the product of sets with the group operation ⟨n₁, g₁⟩ * ⟨n₂, g₂⟩ = ⟨n₁ * φ g₁ n₂, g₁ * g₂⟩

Defined in

Mathlib.GroupTheory.SemidirectProduct

Cited by

69 results in Mathlib

Foundations

Depth 23 from the axioms · uses Quot.sound

Assumes

GroupGroup