Theorems · Theorem · group theory

SemidirectProduct.lift_inr

∀ {N : Type u_1} {G : Type u_2} {H : Type u_3} [inst : Group N] [inst_1 : Group G] [inst_2 : Group H]
  {φ : G →* MulAut N} (fn : N →* H) (fg : G →* H)
  (h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn) (g : G),
  (SemidirectProduct.lift fn fg h) (SemidirectProduct.inr g) = fg g

Defined in

Mathlib.GroupTheory.SemidirectProduct

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupGroupGroup