Structures · Algebra
Subgroup.Normal
A subgroup H is normal if whenever n ∈ H, then g * n * g⁻¹ ∈ H for every g : G
[Wikidata Q743179](https://www.wikidata.org/wiki/Q743179)
- Defined in
- Mathlib.Algebra.Group.Subgroup.Defs
- Shape
- One type argument · adds conj_mem
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances8
- Units
- AlgEquiv
- Equiv.Perm
- Field.absoluteGaloisGroup
- Subtype
- Prod
- MulOpposite
- HasQuotient.Quotient
How is a type an instance?
Loading the hierarchy index…
Assumed by333
- QuotientGroup.mk'
- QuotientGroup.ker_mk'
- QuotientGroup.eq_one_iff
- QuotientGroup.congr
- QuotientGroup.mk'_surjective
- QuotientGroup.map
- Subgroup.normalClosure_le_normal
- MulAut.conjNormal
- QuotientGroup.lift
- Subgroup.upperCentralSeriesStep
- Rep.coinvariantsShortComplex
- Subgroup.normalizer_eq_top
- QuotientGroup.con
- groupHomology.H1CoresCoinfOfTrivial
- MonoidHom.domRestrictHomKerEquiv
- groupHomology.H1CoresCoinf
- groupCohomology.H1InfRes
- QuotientGroup.monoidHom_ext
- Rep.toCoinvariants
- QuotientGroup.quotientMulEquivOfEq
- Subgroup.normal_le_normalCore
- Rep.toCoinvariantsMkQ
- QuotientGroup.coe_mk'
- QuotientGroup.mk_one
- Rep.ofQuotient
- MulAction.IwasawaStructure.commutator_le
- IsGaloisGroup.quotientMulEquiv
- IsPGroup.to_quotient
- Subgroup.commutator_le_right
- QuotientGroup.mk_mul
- Rep.quotientToCoinvariants
- Representation.ofQuotient
- Subgroup.IsComplement'.QuotientMulEquiv
- SemidirectProduct.mulEquivSubgroup
- Representation.quotientToInvariants_lift
- MulAction.coe_quotient_smul
- Subgroup.le_normalizer_of_normal
- Group.exponent_quotient_dvd
- Rep.quotientToInvariants
- Rep.quotientToCoinvariantsFunctor
- QuotientGroup.quotientQuotientEquivQuotientAux
- QuotientGroup.ker_lift
- Subgroup.smul_diff'
- QuotientGroup.map_mk'_self
- QuotientGroup.mk'_eq_mk'
- Subgroup.normalClosure_subset_iff
- Action.FintypeCat.toEndHom
- QuotientGroup.lift_mk'
- Representation.toCoinvariantsKer
- MeasureTheory.Measure.IsMulLeftInvariant.quotientMeasureEqMeasurePreimage_of_set
Ancestors0
No ancestors.