Theorems · Theorem · group theory

SemidirectProduct.map_inr

∀ {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [inst : Group N₁] [inst_1 : Group G₁]
  [inst_2 : Group N₂] [inst_3 : Group G₂] {φ₁ : G₁ →* MulAut N₁} {φ₂ : G₂ →* MulAut N₂} (fn : N₁ →* N₂) (fg : G₁ →* G₂)
  (h : ∀ (g : G₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn) (g : G₁),
  (SemidirectProduct.map fn fg h) (SemidirectProduct.inr g) = SemidirectProduct.inr (fg g)

Defined in

Mathlib.GroupTheory.SemidirectProduct

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupGroupGroupGroup