Structures · Algebra
AddSubgroup.Normal
An AddSubgroup H is normal if whenever n ∈ H, then g + n - g ∈ H for every g : A
[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 instances4
- Subtype
- Prod
- AddOpposite
- HasQuotient.Quotient
How is a type an instance?
Loading the hierarchy index…
Assumed by158
- QuotientAddGroup.mk'
- QuotientAddGroup.eq_zero_iff
- QuotientAddGroup.lift
- QuotientAddGroup.ker_mk'
- QuotientAddGroup.mk_zero
- QuotientAddGroup.mk'_surjective
- QuotientAddGroup.map
- AddSubgroup.normalClosure_le_normal
- QuotientAddGroup.con
- QuotientAddGroup.addMonoidHom_ext
- QuotientAddGroup.lift_mk'
- AddSubgroup.upperCentralSeriesStep
- QuotientAddGroup.mk_nsmul
- QuotientAddGroup.mk_zsmul
- AddSubgroup.normal_le_normalCore
- QuotientAddGroup.eq_iff_sub_mem
- QuotientAddGroup.congr
- AddSubgroup.addCommutator_le_right
- QuotientAddGroup.coe_mk'
- AddSubgroup.le_normalizer_of_normal
- AddSubgroup.nsmul_index_mem
- QuotientAddGroup.mk'_apply
- MeasureTheory.Measure.IsAddLeftInvariant.addQuotientMeasureEqMeasurePreimage_of_set
- QuotientAddGroup.lift_surjective_of_surjective
- AddSubgroup.normalizer_eq_top
- QuotientAddGroup.sound
- MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addInvariantMeasure_quotient
- QuotientAddGroup.liftEquiv
- AddSubgroup.relIndex_sup_right
- FiniteIndexNormalAddSubgroup.ofAddSubgroup
- QuotientAddGroup.prodAddEquiv
- QuotientAddGroup.ker_lift
- AddSubgroup.addCommutator_le_left
- AddSubgroup.normalClosure_eq_self
- AddSubgroup.subset_normalizer_of_normal
- QuotientAddGroup.quotientQuotientEquivQuotientAux
- AddSubgroup.nsmul_relIndex_mem
- AddSubgroup.normalClosure_subset_iff
- QuotientAddGroup.quotientInfEquivSumNormalQuotient
- IsFundamentalDomain.AddQuotientMeasureEqMeasurePreimage_AddHaarMeasure
- QuotientAddGroup.mk_add
- AddSubgroup.normalCore_eq_self
- QuotientAddGroup.quotientAddEquivOfEq
- QuotientAddGroup.map_map
- QuotientAddGroup.map_surjective_of_surjective
- QuotientAddGroup.map_id_apply
- QuotientAddGroup.con_le_iff
- AddSubgroup.Normal.map_addConj_eq
- QuotientAddGroup.preimage_image_coe
- QuotientAddGroup.image_coe_inj
Ancestors0
No ancestors.