Theorems · Definition · group theory
Subgroup.normalizerMonoidHom
{G : Type u_1} → [inst : Group G] → (H : Subgroup G) → ↥(Subgroup.normalizer ↑H) →* MulAut ↥HThe homomorphism N(H) → Aut(H) with kernel C(H).
- Defined in
- Mathlib.GroupTheory.Subgroup.Centralizer
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Group
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SetLike.coestatement and proof · cited by 8,199
- Groupstatement and proof · cited by 6,238
- MonoidHomstatement · cited by 3,629
- Subgroupstatement and proof · cited by 3,593
- MulAutstatement · cited by 158
- Subgroup.normalizerstatement and proof · cited by 108
- MulDistribMulAction.toMulAutproof · cited by 1
Cited by12
Results whose statement or proof uses this declaration.
- SemidirectProduct.mulEquivSubgroupstatement · cited by 3
- Subgroup.normalizerMonoidHom_kerstatement · cited by 2
- IsCyclic.normalizer_le_centralizerproof · cited by 2
- SemidirectProduct.monoidHomSubgroupstatement · cited by 2
- Subgroup.normalizerMonoidHom_apply_apply_coestatement and proof · cited by 1
- IsZGroup.isCyclic_commutatorproof · cited by 1
- IsPGroup.commutator_eq_bot_or_commutator_eq_selfproof · cited by 1
- SemidirectProduct.mulEquivSubgroup_applystatement and proof · cited by 0
- SemidirectProduct.mulEquivSubgroup_symm_applystatement · cited by 0
- Subgroup.normalizerMonoidHom_apply_symm_apply_coestatement · cited by 0
- isZGroup_iff_exists_mulEquivproof · cited by 0
- SemidirectProduct.monoidHomSubgroup_applystatement and proof · cited by 0