Theorems · Definition · group theory
SemidirectProduct.mulEquivSubgroup
{G : Type u_2} →
[inst : Group G] →
{H K : Subgroup G} →
[inst_1 : H.Normal] → H.IsComplement' K → ↥H ⋊[H.normalizerMonoidHom.comp (Subgroup.inclusion ⋯)] ↥K ≃* GThe isomorphism from a semidirect product of complementary subgroups to the ambient group.
- Defined in
- Mathlib.GroupTheory.SemidirectProduct
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- GroupSubgroup.Normal
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Top.topstatement · cited by 9,680
- SetLike.coestatement · cited by 8,199
- Groupstatement and proof · cited by 6,238
- Subgroupstatement and proof · cited by 3,593
- MulEquivstatement · cited by 1,142
- MonoidHom.compstatement · cited by 469
- le_topstatement · cited by 411
- Subgroup.Normalstatement and proof · cited by 334
- MulAutstatement · cited by 158
- Subgroup.normalizerstatement · cited by 108
- SemidirectProductstatement · cited by 69
- Subgroup.IsComplement'statement and proof · cited by 34
Cited by3
Results whose statement or proof uses this declaration.
- SemidirectProduct.mulEquivSubgroup_applystatement and proof · cited by 0
- SemidirectProduct.mulEquivSubgroup_symm_applystatement and proof · cited by 0
- isZGroup_iff_exists_mulEquivproof · cited by 0