Theorems · Theorem · group theory

SemidirectProduct.map.congr_simp

∀ {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 fn_1 : N₁ →* N₂)
  (e_fn : fn = fn_1) (fg fg_1 : G₁ →* G₂) (e_fg : fg = fg_1)
  (h : ∀ (g : G₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn),
  SemidirectProduct.map fn fg h = SemidirectProduct.map fn_1 fg_1 ⋯

Defined in

Mathlib.GroupTheory.SemidirectProduct

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupGroupGroupGroup