Theorems · Theorem · group theory

SemidirectProduct.mulEquivSubgroup_symm_apply

∀ {G : Type u_2} [inst : Group G] {H K : Subgroup G} [inst_1 : H.Normal] (h : H.IsComplement' K) (b : G),
  (SemidirectProduct.mulEquivSubgroup h).symm b = Function.surjInv ⋯ b

Defined in

Mathlib.GroupTheory.SemidirectProduct

Cited by

0 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupSubgroup.Normal