Basic

📁 Source: Mathlib/GroupTheory/QuotientGroup/Basic.lean

Statistics

Metric	Count
Definitions restrictHomKerEquiv, restrictHomKerEquiv, comapMk'OrderIso, equivQuotientAddSubgroupOfOfEq, equivQuotientZSMulOfEquiv, homQuotientZSMulOfHom, kerLift, quotientAddEquivOfEq, quotientBot, quotientInfEquivSumNormalQuotient, quotientInfEquivSumNormalizerQuotient, quotientKerEquivOfRightInverse, quotientKerEquivOfSurjective, quotientKerEquivRange, quotientMapAddSubgroupOfOfLe, quotientQuotientEquivQuotient, quotientQuotientEquivQuotientAux, rangeKerLift, comapMk'OrderIso, equivQuotientSubgroupOfOfEq, equivQuotientZPowOfEquiv, homQuotientZPowOfHom, kerLift, quotientBot, quotientInfEquivProdNormalQuotient, quotientInfEquivProdNormalizerQuotient, quotientKerEquivOfRightInverse, quotientKerEquivOfSurjective, quotientKerEquivRange, quotientMapSubgroupOfOfLe, quotientMulEquivOfEq, quotientQuotientEquivQuotient, quotientQuotientEquivQuotientAux, rangeKerLift	34
Theorems comap_quotient_mk, restrictHomKerEquiv_apply_coe, restrictHomKerEquiv_symm_coe_apply, addSubgroup_eq_top_of_subsingleton, comap_comap_center, comap_map_mk', equivQuotientZSMulOfEquiv_refl, equivQuotientZSMulOfEquiv_symm, equivQuotientZSMulOfEquiv_trans, homQuotientZSMulOfHom_comp, homQuotientZSMulOfHom_comp_of_rightInverse, homQuotientZSMulOfHom_id, kerLift_injective, kerLift_mk, kerLift_mk', le_comap_mk', map_normal, mk_int_mul, mk_nat_mul, mk_sum, quotientAddEquivOfEq_mk, quotientBot_apply, quotientBot_symm_apply, quotientKerEquivOfRightInverse_apply, quotientKerEquivOfRightInverse_symm_apply, quotientMapAddSubgroupOfOfLe_mk, quotientQuotientEquivQuotientAux_mk, quotientQuotientEquivQuotientAux_mk_mk, rangeKerLift_injective, rangeKerLift_surjective, sound, strictMono_comap_prod_map, subsingleton_quotient_top, comap_comap_center, comap_map_mk', equivQuotientZPowOfEquiv_refl, equivQuotientZPowOfEquiv_symm, equivQuotientZPowOfEquiv_trans, homQuotientZPowOfHom_comp, homQuotientZPowOfHom_comp_of_rightInverse, homQuotientZPowOfHom_id, kerLift_injective, kerLift_mk, kerLift_mk', le_comap_mk', map_normal, mk_prod, quotientBot_apply, quotientBot_symm_apply, quotientKerEquivOfRightInverse_apply, quotientKerEquivOfRightInverse_symm_apply, quotientMapSubgroupOfOfLe_mk, quotientMulEquivOfEq_mk, quotientQuotientEquivQuotientAux_mk, quotientQuotientEquivQuotientAux_mk_mk, rangeKerLift_injective, rangeKerLift_surjective, sound, strictMono_comap_prod_map, subgroup_eq_top_of_subsingleton, subsingleton_quotient_top, comap_quotient_mk	62
Total	96

AddMonoidHom

Definitions

Name	Category	Theorems
restrictHomKerEquiv 📖	CompOp	—

AddSubgroup.Characteristic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_quotient_mk 📖	mathematical	—	AddSubgroup.Characteristic AddSubgroup.comap HasQuotient.Quotient AddSubgroup QuotientAddGroup.instHasQuotientAddSubgroup QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_characteristic QuotientAddGroup.mk'	—	AddSubgroup.normal_of_characteristic AddSubgroup.characteristic_iff_comap_eq AddSubgroup.characteristic_iff_map_eq

MonoidHom

Definitions

Name	Category	Theorems
restrictHomKerEquiv 📖	CompOp	2 math math: restrictHomKerEquiv_apply_coe, restrictHomKerEquiv_symm_coe_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrictHomKerEquiv_apply_coe 📖	mathematical	—	DFunLike.coe MonoidHom HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid QuotientGroup.Quotient.group CommGroup.toGroup instFunLike MulEquiv CommMonoid.toMonoid CommGroup.toCommMonoid instCommGroup SetLike.instMembership Subgroup.instSetLike ker SubmonoidClass.toMulOneClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass Subgroup.toGroup restrictHom Subgroup.mul mul EquivLike.toFunLike MulEquiv.instEquivLike restrictHomKerEquiv	—	SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass
restrictHomKerEquiv_symm_coe_apply 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommMonoid.toMonoid CommGroup.toCommMonoid instFunLike Subgroup CommGroup.toGroup instCommGroup SetLike.instMembership Subgroup.instSetLike ker SubmonoidClass.toMulOneClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass Subgroup.toGroup restrictHom MulEquiv HasQuotient.Quotient QuotientGroup.instHasQuotientSubgroup QuotientGroup.Quotient.group mul Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm restrictHomKerEquiv	—	SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass

QuotientAddGroup

Definitions

Name	Category	Theorems
comapMk'OrderIso 📖	CompOp	—
equivQuotientAddSubgroupOfOfEq 📖	CompOp	—
equivQuotientZSMulOfEquiv 📖	CompOp	3 math math: equivQuotientZSMulOfEquiv_symm, equivQuotientZSMulOfEquiv_trans, equivQuotientZSMulOfEquiv_refl
homQuotientZSMulOfHom 📖	CompOp	3 math math: homQuotientZSMulOfHom_comp_of_rightInverse, homQuotientZSMulOfHom_comp, homQuotientZSMulOfHom_id
kerLift 📖	CompOp	5 math math: kerLift_mk, quotientBot_apply, quotientKerEquivOfRightInverse_apply, kerLift_mk', kerLift_injective
quotientAddEquivOfEq 📖	CompOp	1 math math: quotientAddEquivOfEq_mk
quotientBot 📖	CompOp	2 math math: quotientBot_apply, quotientBot_symm_apply
quotientInfEquivSumNormalQuotient 📖	CompOp	—
quotientInfEquivSumNormalizerQuotient 📖	CompOp	—
quotientKerEquivOfRightInverse 📖	CompOp	2 math math: quotientKerEquivOfRightInverse_symm_apply, quotientKerEquivOfRightInverse_apply
quotientKerEquivOfSurjective 📖	CompOp	—
quotientKerEquivRange 📖	CompOp	—
quotientMapAddSubgroupOfOfLe 📖	CompOp	1 math math: quotientMapAddSubgroupOfOfLe_mk
quotientQuotientEquivQuotient 📖	CompOp	—
quotientQuotientEquivQuotientAux 📖	CompOp	2 math math: quotientQuotientEquivQuotientAux_mk, quotientQuotientEquivQuotientAux_mk_mk
rangeKerLift 📖	CompOp	2 math math: rangeKerLift_injective, rangeKerLift_surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addSubgroup_eq_top_of_subsingleton 📖	mathematical	—	Top.top AddSubgroup AddSubgroup.instTop	—	top_unique eq zero_add neg_zero
comap_comap_center 📖	mathematical	—	AddSubgroup.comap HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup Quotient.addGroup mk' AddSubgroup.center AddSubgroup.normal_comap	—	AddSubgroup.ext AddSubgroup.normal_comap AddSubgroup.mem_comap AddSubgroup.mem_center_iff eq_iff_sub_mem
comap_map_mk' 📖	mathematical	—	AddSubgroup.comap HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup Quotient.addGroup mk' AddSubgroup.map SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice AddSubgroup.instCompleteLattice	—	AddSubgroup.comap_map_eq ker_mk' sup_comm
equivQuotientZSMulOfEquiv_refl 📖	mathematical	—	AddEquiv.refl HasQuotient.Quotient AddSubgroup AddCommGroup.toAddGroup instHasQuotientAddSubgroup AddMonoidHom.range zsmulAddGroupHom AddCommGroup.toDivisionAddCommMonoid AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Quotient.addGroup AddSubgroup.normal_of_comm equivQuotientZSMulOfEquiv	—	AddEquiv.ext AddSubgroup.normal_of_comm Quotient.out_eq'
equivQuotientZSMulOfEquiv_symm 📖	mathematical	—	AddEquiv.symm HasQuotient.Quotient AddSubgroup AddCommGroup.toAddGroup instHasQuotientAddSubgroup AddMonoidHom.range zsmulAddGroupHom AddCommGroup.toDivisionAddCommMonoid AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Quotient.addGroup AddSubgroup.normal_of_comm equivQuotientZSMulOfEquiv	—	AddSubgroup.normal_of_comm
equivQuotientZSMulOfEquiv_trans 📖	mathematical	—	AddEquiv.trans HasQuotient.Quotient AddSubgroup AddCommGroup.toAddGroup instHasQuotientAddSubgroup AddMonoidHom.range zsmulAddGroupHom AddCommGroup.toDivisionAddCommMonoid AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Quotient.addGroup AddSubgroup.normal_of_comm equivQuotientZSMulOfEquiv	—	AddEquiv.ext AddSubgroup.normal_of_comm Quotient.out_eq'
homQuotientZSMulOfHom_comp 📖	mathematical	—	homQuotientZSMulOfHom AddMonoidHom.comp AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup AddMonoidHom.range zsmulAddGroupHom AddCommGroup.toDivisionAddCommMonoid Quotient.addGroup AddSubgroup.normal_of_comm	—	addMonoidHom_ext AddSubgroup.normal_of_comm
homQuotientZSMulOfHom_comp_of_rightInverse 📖	mathematical	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddMonoidHom.instFunLike	AddMonoidHom.comp HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup AddMonoidHom.range zsmulAddGroupHom AddCommGroup.toDivisionAddCommMonoid Quotient.addGroup AddSubgroup.normal_of_comm homQuotientZSMulOfHom AddMonoidHom.id	—	addMonoidHom_ext AddSubgroup.normal_of_comm AddMonoidHom.ext
homQuotientZSMulOfHom_id 📖	mathematical	—	homQuotientZSMulOfHom AddMonoidHom.id AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup AddMonoidHom.range zsmulAddGroupHom AddCommGroup.toDivisionAddCommMonoid Quotient.addGroup AddSubgroup.normal_of_comm	—	addMonoidHom_ext AddSubgroup.normal_of_comm
kerLift_injective 📖	mathematical	—	HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup AddMonoidHom.ker AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DFunLike.coe AddMonoidHom AddZeroClass.toAddZero Quotient.addGroup AddMonoidHom.normal_ker AddMonoidHom.instFunLike kerLift	—	Quotient.inductionOn₂' AddMonoidHom.normal_ker Quotient.sound' leftRel_apply AddMonoidHom.mem_ker AddMonoidHom.map_add AddMonoidHom.map_neg neg_add_cancel
kerLift_mk 📖	mathematical	—	DFunLike.coe AddMonoidHom HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup AddMonoidHom.ker AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddZeroClass.toAddZero Quotient.addGroup AddMonoidHom.normal_ker AddMonoidHom.instFunLike kerLift	—	AddMonoidHom.normal_ker
kerLift_mk' 📖	mathematical	—	DFunLike.coe AddMonoidHom HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup AddMonoidHom.ker AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddZeroClass.toAddZero Quotient.addGroup AddMonoidHom.normal_ker AddMonoidHom.instFunLike kerLift	—	—
le_comap_mk' 📖	mathematical	—	AddSubgroup Preorder.toLE PartialOrder.toPreorder AddSubgroup.instPartialOrder AddSubgroup.comap HasQuotient.Quotient instHasQuotientAddSubgroup Quotient.addGroup mk'	—	ker_mk' AddSubgroup.comap_mono bot_le
map_normal 📖	mathematical	—	AddSubgroup.Normal HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup Quotient.addGroup AddSubgroup.map mk'	—	AddSubgroup.Normal.map mk_surjective
mk_int_mul 📖	mathematical	—	AddGroupWithOne.toAddGroup AddCommGroupWithOne.toAddGroupWithOne NonAssocRing.toAddCommGroupWithOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing AddGroupWithOne.toIntCast HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup SubNegMonoid.toZSMul AddGroup.toSubNegMonoid Quotient.addGroup	—	zsmul_eq_mul mk_zsmul
mk_nat_mul 📖	mathematical	—	AddGroupWithOne.toAddGroup AddCommGroupWithOne.toAddGroupWithOne NonAssocRing.toAddCommGroupWithOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Quotient.addGroup	—	nsmul_eq_mul mk_nsmul
mk_sum 📖	mathematical	—	AddCommGroup.toAddGroup Finset.sum AddCommGroup.toAddCommMonoid HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup Quotient.addCommGroup	—	map_sum AddSubgroup.normal_of_comm AddMonoidHom.instAddMonoidHomClass
quotientAddEquivOfEq_mk 📖	mathematical	—	DFunLike.coe AddEquiv HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Quotient.addGroup EquivLike.toFunLike AddEquiv.instEquivLike quotientAddEquivOfEq	—	—
quotientBot_apply 📖	mathematical	—	DFunLike.coe AddEquiv HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup Bot.bot AddSubgroup.instBot AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Quotient.addGroup AddSubgroup.normal_bot EquivLike.toFunLike AddEquiv.instEquivLike quotientBot AddMonoidHom AddMonoidHom.id AddMonoidHom.instFunLike kerLift	—	AddSubgroup.normal_bot
quotientBot_symm_apply 📖	mathematical	—	DFunLike.coe AddEquiv HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup Bot.bot AddSubgroup.instBot AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Quotient.addGroup AddSubgroup.normal_bot EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm quotientBot	—	AddSubgroup.normal_bot
quotientKerEquivOfRightInverse_apply 📖	mathematical	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddMonoidHom.instFunLike	AddEquiv HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup AddMonoidHom.ker AddZero.toAdd Quotient.addGroup AddMonoidHom.normal_ker EquivLike.toFunLike AddEquiv.instEquivLike quotientKerEquivOfRightInverse kerLift	—	AddMonoidHom.normal_ker
quotientKerEquivOfRightInverse_symm_apply 📖	mathematical	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddMonoidHom.instFunLike	AddEquiv HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup AddMonoidHom.ker AddZero.toAdd Quotient.addGroup AddMonoidHom.normal_ker EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm quotientKerEquivOfRightInverse	—	AddMonoidHom.normal_ker
quotientMapAddSubgroupOfOfLe_mk 📖	mathematical	AddSubgroup Preorder.toLE PartialOrder.toPreorder AddSubgroup.instPartialOrder	DFunLike.coe AddMonoidHom HasQuotient.Quotient SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.toAddGroup instHasQuotientAddSubgroup AddSubgroup.addSubgroupOf AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Quotient.addGroup AddMonoidHom.instFunLike quotientMapAddSubgroupOfOfLe AddSubgroup.inclusion	—	—
quotientQuotientEquivQuotientAux_mk 📖	mathematical	AddSubgroup Preorder.toLE PartialOrder.toPreorder AddSubgroup.instPartialOrder	DFunLike.coe AddMonoidHom HasQuotient.Quotient instHasQuotientAddSubgroup Quotient.addGroup AddSubgroup.map mk' AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid map_normal AddMonoidHom.instFunLike quotientQuotientEquivQuotientAux map AddMonoidHom.id	—	lift_mk' map_normal
quotientQuotientEquivQuotientAux_mk_mk 📖	mathematical	AddSubgroup Preorder.toLE PartialOrder.toPreorder AddSubgroup.instPartialOrder	DFunLike.coe AddMonoidHom HasQuotient.Quotient instHasQuotientAddSubgroup Quotient.addGroup AddSubgroup.map mk' AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid map_normal AddMonoidHom.instFunLike quotientQuotientEquivQuotientAux	—	lift_mk' map_normal
rangeKerLift_injective 📖	mathematical	—	HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup AddMonoidHom.ker AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SetLike.instMembership AddSubgroup.instSetLike AddMonoidHom.range DFunLike.coe AddMonoidHom AddZeroClass.toAddZero Quotient.addGroup AddMonoidHom.normal_ker AddSubgroup.toAddGroup AddMonoidHom.instFunLike rangeKerLift	—	Quotient.inductionOn₂' AddMonoidHom.normal_ker Quotient.sound' leftRel_apply AddMonoidHom.ker_rangeRestrict AddMonoidHom.mem_ker AddMonoidHom.map_add AddMonoidHom.map_neg neg_add_cancel
rangeKerLift_surjective 📖	mathematical	—	HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup AddMonoidHom.ker AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SetLike.instMembership AddSubgroup.instSetLike AddMonoidHom.range DFunLike.coe AddMonoidHom AddZeroClass.toAddZero Quotient.addGroup AddMonoidHom.normal_ker AddSubgroup.toAddGroup AddMonoidHom.instFunLike rangeKerLift	—	AddMonoidHom.normal_ker
sound 📖	mathematical	—	HVAdd.hVAdd AddOpposite AddSubgroup AddOpposite.instAddGroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.op Set instHVAdd Set.vaddSet AddSubgroup.instVAdd Set.preimage HasQuotient.Quotient instHasQuotientAddSubgroup DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Quotient.addGroup AddMonoidHom.instFunLike mk'	—	Set.ext Set.mem_vadd_set_iff_neg_vadd_mem Set.mem_preimage
strictMono_comap_prod_map 📖	mathematical	—	StrictMono AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.toAddGroup HasQuotient.Quotient instHasQuotientAddSubgroup Quotient.addGroup PartialOrder.toPreorder AddSubgroup.instPartialOrder Prod.instPreorder AddSubgroup.comap AddSubgroup.subtype AddSubgroup.map mk'	—	strictMono_comap_prod_image
subsingleton_quotient_top 📖	mathematical	—	HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup Top.top AddSubgroup.instTop	—	subsingleton_iff

QuotientGroup

Definitions

Name	Category	Theorems
comapMk'OrderIso 📖	CompOp	—
equivQuotientSubgroupOfOfEq 📖	CompOp	—
equivQuotientZPowOfEquiv 📖	CompOp	3 math math: equivQuotientZPowOfEquiv_trans, equivQuotientZPowOfEquiv_refl, equivQuotientZPowOfEquiv_symm
homQuotientZPowOfHom 📖	CompOp	3 math math: homQuotientZPowOfHom_id, homQuotientZPowOfHom_comp_of_rightInverse, homQuotientZPowOfHom_comp
kerLift 📖	CompOp	5 math math: kerLift_mk, kerLift_mk', quotientKerEquivOfRightInverse_apply, kerLift_injective, quotientBot_apply
quotientBot 📖	CompOp	2 math math: quotientBot_apply, quotientBot_symm_apply
quotientInfEquivProdNormalQuotient 📖	CompOp	—
quotientInfEquivProdNormalizerQuotient 📖	CompOp	—
quotientKerEquivOfRightInverse 📖	CompOp	2 math math: quotientKerEquivOfRightInverse_apply, quotientKerEquivOfRightInverse_symm_apply
quotientKerEquivOfSurjective 📖	CompOp	—
quotientKerEquivRange 📖	CompOp	4 math math: Submodule.unitsQuotEquivRelPic_symm_apply, ClassGroup.equivPic_symm_apply, ClassGroup.equivPic_apply, Submodule.unitsQuotEquivRelPic_apply_coe
quotientMapSubgroupOfOfLe 📖	CompOp	1 math math: quotientMapSubgroupOfOfLe_mk
quotientMulEquivOfEq 📖	CompOp	1 math math: quotientMulEquivOfEq_mk
quotientQuotientEquivQuotient 📖	CompOp	—
quotientQuotientEquivQuotientAux 📖	CompOp	2 math math: quotientQuotientEquivQuotientAux_mk, quotientQuotientEquivQuotientAux_mk_mk
rangeKerLift 📖	CompOp	2 math math: rangeKerLift_injective, rangeKerLift_surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_comap_center 📖	mathematical	—	Subgroup.comap HasQuotient.Quotient Subgroup instHasQuotientSubgroup Quotient.group mk' Subgroup.center Subgroup.normal_comap	—	Subgroup.ext Subgroup.normal_comap
comap_map_mk' 📖	mathematical	—	Subgroup.comap HasQuotient.Quotient Subgroup instHasQuotientSubgroup Quotient.group mk' Subgroup.map SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Subgroup.instCompleteLattice	—	Subgroup.comap_map_eq ker_mk' sup_comm
equivQuotientZPowOfEquiv_refl 📖	mathematical	—	MulEquiv.refl HasQuotient.Quotient Subgroup CommGroup.toGroup instHasQuotientSubgroup MonoidHom.range zpowGroupHom CommGroup.toDivisionCommMonoid MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Quotient.group Subgroup.normal_of_comm equivQuotientZPowOfEquiv	—	MulEquiv.ext Subgroup.normal_of_comm Quotient.out_eq'
equivQuotientZPowOfEquiv_symm 📖	mathematical	—	MulEquiv.symm HasQuotient.Quotient Subgroup CommGroup.toGroup instHasQuotientSubgroup MonoidHom.range zpowGroupHom CommGroup.toDivisionCommMonoid MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Quotient.group Subgroup.normal_of_comm equivQuotientZPowOfEquiv	—	Subgroup.normal_of_comm
equivQuotientZPowOfEquiv_trans 📖	mathematical	—	MulEquiv.trans HasQuotient.Quotient Subgroup CommGroup.toGroup instHasQuotientSubgroup MonoidHom.range zpowGroupHom CommGroup.toDivisionCommMonoid MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Quotient.group Subgroup.normal_of_comm equivQuotientZPowOfEquiv	—	MulEquiv.ext Subgroup.normal_of_comm Quotient.out_eq'
homQuotientZPowOfHom_comp 📖	mathematical	—	homQuotientZPowOfHom MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup HasQuotient.Quotient Subgroup instHasQuotientSubgroup MonoidHom.range zpowGroupHom CommGroup.toDivisionCommMonoid Quotient.group Subgroup.normal_of_comm	—	monoidHom_ext Subgroup.normal_of_comm
homQuotientZPowOfHom_comp_of_rightInverse 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MonoidHom.instFunLike	MonoidHom.comp HasQuotient.Quotient Subgroup instHasQuotientSubgroup MonoidHom.range zpowGroupHom CommGroup.toDivisionCommMonoid Quotient.group Subgroup.normal_of_comm homQuotientZPowOfHom MonoidHom.id	—	monoidHom_ext Subgroup.normal_of_comm MonoidHom.ext
homQuotientZPowOfHom_id 📖	mathematical	—	homQuotientZPowOfHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup HasQuotient.Quotient Subgroup instHasQuotientSubgroup MonoidHom.range zpowGroupHom CommGroup.toDivisionCommMonoid Quotient.group Subgroup.normal_of_comm	—	monoidHom_ext Subgroup.normal_of_comm
kerLift_injective 📖	mathematical	—	HasQuotient.Quotient Subgroup instHasQuotientSubgroup MonoidHom.ker Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid DFunLike.coe MonoidHom MulOneClass.toMulOne Quotient.group MonoidHom.normal_ker MonoidHom.instFunLike kerLift	—	Quotient.inductionOn₂' MonoidHom.normal_ker Quotient.sound' leftRel_apply MonoidHom.mem_ker MonoidHom.map_mul MonoidHom.map_inv inv_mul_cancel
kerLift_mk 📖	mathematical	—	DFunLike.coe MonoidHom HasQuotient.Quotient Subgroup instHasQuotientSubgroup MonoidHom.ker Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulOneClass.toMulOne Quotient.group MonoidHom.normal_ker MonoidHom.instFunLike kerLift	—	MonoidHom.normal_ker
kerLift_mk' 📖	mathematical	—	DFunLike.coe MonoidHom HasQuotient.Quotient Subgroup instHasQuotientSubgroup MonoidHom.ker Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulOneClass.toMulOne Quotient.group MonoidHom.normal_ker MonoidHom.instFunLike kerLift	—	—
le_comap_mk' 📖	mathematical	—	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder Subgroup.comap HasQuotient.Quotient instHasQuotientSubgroup Quotient.group mk'	—	ker_mk' Subgroup.comap_mono bot_le
map_normal 📖	mathematical	—	Subgroup.Normal HasQuotient.Quotient Subgroup instHasQuotientSubgroup Quotient.group Subgroup.map mk'	—	Subgroup.Normal.map mk_surjective
mk_prod 📖	mathematical	—	CommGroup.toGroup Finset.prod CommGroup.toCommMonoid HasQuotient.Quotient Subgroup instHasQuotientSubgroup Quotient.commGroup	—	map_prod Subgroup.normal_of_comm MonoidHom.instMonoidHomClass
quotientBot_apply 📖	mathematical	—	DFunLike.coe MulEquiv HasQuotient.Quotient Subgroup instHasQuotientSubgroup Bot.bot Subgroup.instBot MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Quotient.group Subgroup.normal_bot EquivLike.toFunLike MulEquiv.instEquivLike quotientBot MonoidHom MonoidHom.id MonoidHom.instFunLike kerLift	—	Subgroup.normal_bot
quotientBot_symm_apply 📖	mathematical	—	DFunLike.coe MulEquiv HasQuotient.Quotient Subgroup instHasQuotientSubgroup Bot.bot Subgroup.instBot MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Quotient.group Subgroup.normal_bot EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm quotientBot	—	Subgroup.normal_bot
quotientKerEquivOfRightInverse_apply 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	MulEquiv HasQuotient.Quotient Subgroup instHasQuotientSubgroup MonoidHom.ker MulOne.toMul Quotient.group MonoidHom.normal_ker EquivLike.toFunLike MulEquiv.instEquivLike quotientKerEquivOfRightInverse kerLift	—	MonoidHom.normal_ker
quotientKerEquivOfRightInverse_symm_apply 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	MulEquiv HasQuotient.Quotient Subgroup instHasQuotientSubgroup MonoidHom.ker MulOne.toMul Quotient.group MonoidHom.normal_ker EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm quotientKerEquivOfRightInverse	—	MonoidHom.normal_ker
quotientMapSubgroupOfOfLe_mk 📖	mathematical	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder	DFunLike.coe MonoidHom HasQuotient.Quotient SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup instHasQuotientSubgroup Subgroup.subgroupOf MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Quotient.group MonoidHom.instFunLike quotientMapSubgroupOfOfLe Subgroup.inclusion	—	—
quotientMulEquivOfEq_mk 📖	mathematical	—	DFunLike.coe MulEquiv HasQuotient.Quotient Subgroup instHasQuotientSubgroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Quotient.group EquivLike.toFunLike MulEquiv.instEquivLike quotientMulEquivOfEq	—	—
quotientQuotientEquivQuotientAux_mk 📖	mathematical	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder	DFunLike.coe MonoidHom HasQuotient.Quotient instHasQuotientSubgroup Quotient.group Subgroup.map mk' MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid map_normal MonoidHom.instFunLike quotientQuotientEquivQuotientAux map MonoidHom.id	—	lift_mk' map_normal
quotientQuotientEquivQuotientAux_mk_mk 📖	mathematical	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder	DFunLike.coe MonoidHom HasQuotient.Quotient instHasQuotientSubgroup Quotient.group Subgroup.map mk' MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid map_normal MonoidHom.instFunLike quotientQuotientEquivQuotientAux	—	lift_mk' map_normal
rangeKerLift_injective 📖	mathematical	—	HasQuotient.Quotient Subgroup instHasQuotientSubgroup MonoidHom.ker Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SetLike.instMembership Subgroup.instSetLike MonoidHom.range DFunLike.coe MonoidHom MulOneClass.toMulOne Quotient.group MonoidHom.normal_ker Subgroup.toGroup MonoidHom.instFunLike rangeKerLift	—	Quotient.inductionOn₂' MonoidHom.normal_ker Quotient.sound' leftRel_apply MonoidHom.ker_rangeRestrict MonoidHom.mem_ker MonoidHom.map_mul MonoidHom.map_inv inv_mul_cancel
rangeKerLift_surjective 📖	mathematical	—	HasQuotient.Quotient Subgroup instHasQuotientSubgroup MonoidHom.ker Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SetLike.instMembership Subgroup.instSetLike MonoidHom.range DFunLike.coe MonoidHom MulOneClass.toMulOne Quotient.group MonoidHom.normal_ker Subgroup.toGroup MonoidHom.instFunLike rangeKerLift	—	MonoidHom.normal_ker
sound 📖	mathematical	—	MulOpposite Subgroup MulOpposite.instGroup SetLike.instMembership Subgroup.instSetLike Subgroup.op Set Set.smulSet Subgroup.instSMul Set.preimage HasQuotient.Quotient instHasQuotientSubgroup DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Quotient.group MonoidHom.instFunLike mk'	—	Set.ext
strictMono_comap_prod_map 📖	mathematical	—	StrictMono Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup HasQuotient.Quotient instHasQuotientSubgroup Quotient.group PartialOrder.toPreorder Subgroup.instPartialOrder Prod.instPreorder Subgroup.comap Subgroup.subtype Subgroup.map mk'	—	strictMono_comap_prod_image
subgroup_eq_top_of_subsingleton 📖	mathematical	—	Top.top Subgroup Subgroup.instTop	—	top_unique eq one_mul inv_one
subsingleton_quotient_top 📖	mathematical	—	HasQuotient.Quotient Subgroup instHasQuotientSubgroup Top.top Subgroup.instTop	—	—

Subgroup.Characteristic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_quotient_mk 📖	mathematical	—	Subgroup.Characteristic Subgroup.comap HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup QuotientGroup.Quotient.group Subgroup.normal_of_characteristic QuotientGroup.mk'	—	Subgroup.normal_of_characteristic Subgroup.characteristic_iff_comap_eq Subgroup.characteristic_iff_map_eq

---

← Back to Index