Theorems · Theorem · group theory
Subgroup.Normal.conj_mem
∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.Normal → ∀ n ∈ H, ∀ (g : G), g * n * g⁻¹ ∈ HH is closed under conjugation
- Defined in
- Mathlib.Algebra.Group.Subgroup.Defs
- Cited by
- 23 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext
- Assumes
- Group
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Groupstatement and proof · cited by 6,238
- Subgroupstatement and proof · cited by 3,593
- Subgroup.Normalstatement and proof · cited by 334
Cited by23
Results whose statement or proof uses this declaration.
- Subgroup.normalizer_eq_top_iffproof · cited by 10
- Subgroup.Normal.conj_mem'proof · cited by 7
- Subgroup.normal_le_normalCoreproof · cited by 5
- Subgroup.upperCentralSeries_monoproof · cited by 5
- Subgroup.commutator_le_rightproof · cited by 4
- Subgroup.Normal.comapproof · cited by 3
- Subgroup.Normal.mem_commproof · cited by 2
- Subgroup.normal_iInf_normalproof · cited by 2
- Equiv.Perm.not_isSolvable_fin_5proof · cited by 2
- Subgroup.Normal.conjActproof · cited by 2
- CategoryTheory.PreGaloisCategory.exists_lift_of_quotient_openSubgroupproof · cited by 1
- MulAction.smul_orbit_eq_orbit_smulproof · cited by 1