Defs

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

Statistics

Metric	Count
Definitions `addSubgroup`, `orderIsoAddCon`, `subgroup`, `addCommGroup`, `addGroup`, `con`, `liftEquiv`, `map`, `mk'`, `commGroup`, `group`, `con`, `liftEquiv`, `map`, `mk'`, `orderIsoCon`	16
Theorems `addSubgroup_quotientAddGroupCon`, `mem_addSubgroup_iff`, `orderIsoAddCon_apply`, `orderIsoAddCon_symm_apply_coe`, `mem_subgroup_iff`, `subgroup_quotientGroupCon`, `addMonoidHom_ext`, `addMonoidHom_ext_iff`, `coe_mk'`, `con_addSubgroup`, `con_ker_eq_addConKer`, `con_le_iff`, `con_mono`, `eq_iff_sub_mem`, `eq_zero_iff`, `image_coe`, `image_coe_inj`, `instNormalAddSubgroup`, `ker_le_range_iff`, `ker_lift`, `ker_map`, `ker_mk'`, `leftRel_eq_top`, `liftEquiv_coe`, `liftEquiv_mk`, `lift_comp_mk'`, `lift_mk`, `lift_mk'`, `lift_quot_mk`, `lift_surjective_of_surjective`, `map_comp_map`, `map_id`, `map_id_apply`, `map_map`, `map_mk`, `map_mk'`, `map_mk'_self`, `map_surjective_of_surjective`, `mk'_apply`, `mk'_comp_subtype`, `mk'_eq_mk'`, `mk'_surjective`, `mk_add`, `mk_neg`, `mk_nsmul`, `mk_sub`, `mk_zero`, `mk_zsmul`, `nontrivial_iff`, `preimage_image_coe`, `range_mk'`, `rightRel_eq_top`, `subsingleton_iff`, `coe_mk'`, `con_ker_eq_conKer`, `con_le_iff`, `con_mono`, `con_subgroup`, `congr_apply`, `congr_mk`, `congr_mk'`, `congr_refl`, `congr_symm`, `eq_iff_div_mem`, `eq_one_iff`, `image_coe`, `image_coe_inj`, `instNormalSubgroup`, `ker_le_range_iff`, `ker_lift`, `ker_map`, `ker_mk'`, `leftRel_eq_top`, `liftEquiv_coe`, `liftEquiv_mk`, `lift_comp_mk'`, `lift_mk`, `lift_mk'`, `lift_quot_mk`, `lift_surjective_of_surjective`, `map_comp_map`, `map_id`, `map_id_apply`, `map_map`, `map_mk`, `map_mk'`, `map_mk'_self`, `map_surjective_of_surjective`, `mk'_apply`, `mk'_comp_subtype`, `mk'_eq_mk'`, `mk'_surjective`, `mk_div`, `mk_inv`, `mk_mul`, `mk_one`, `mk_pow`, `mk_zpow`, `monoidHom_ext`, `monoidHom_ext_iff`, `nontrivial_iff`, `preimage_image_coe`, `range_mk'`, `rightRel_eq_top`, `subsingleton_iff`, `orderIsoCon_apply`, `orderIsoCon_symm_apply_coe`	107
Total	123

AddCon

Definitions

Name	Category	Theorems
`addSubgroup` 📖	CompOp	5 math math: `mem_addSubgroup_iff`, `AddSubgroup.orderIsoAddCon_symm_apply_coe`, `addSubgroup_quotientAddGroupCon`, `QuotientAddGroup.instNormalAddSubgroup`, `QuotientAddGroup.con_addSubgroup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addSubgroup_quotientAddGroupCon` 📖	mathematical	—	`addSubgroup` `QuotientAddGroup.con`	—	`AddSubgroup.ext` `mem_addSubgroup_iff` `QuotientAddGroup.leftRel_apply` `add_zero` `neg_mem_iff` `AddSubgroupClass.toNegMemClass` `AddSubgroup.instAddSubgroupClass`
`mem_addSubgroup_iff` 📖	mathematical	—	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `addSubgroup` `DFunLike.coe` `AddCon` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instFunLikeForallProp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—

AddSubgroup

Definitions

Name	Category	Theorems
`orderIsoAddCon` 📖	CompOp	2 math math: `orderIsoAddCon_symm_apply_coe`, `orderIsoAddCon_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`orderIsoAddCon_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `AddSubgroup` `Normal` `AddCon` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `AddCon.instLE` `RelIso.instFunLike` `orderIsoAddCon` `QuotientAddGroup.con`	—	—
`orderIsoAddCon_symm_apply_coe` 📖	mathematical	—	`AddSubgroup` `Normal` `DFunLike.coe` `RelIso` `AddCon` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCon.instLE` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `RelIso.instFunLike` `RelIso.symm` `orderIsoAddCon` `AddCon.addSubgroup`	—	—

Con

Definitions

Name	Category	Theorems
`subgroup` 📖	CompOp	5 math math: `QuotientGroup.con_subgroup`, `mem_subgroup_iff`, `QuotientGroup.instNormalSubgroup`, `subgroup_quotientGroupCon`, `Subgroup.orderIsoCon_symm_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_subgroup_iff` 📖	mathematical	—	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `subgroup` `DFunLike.coe` `Con` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instFunLikeForallProp` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`subgroup_quotientGroupCon` 📖	mathematical	—	`subgroup` `QuotientGroup.con`	—	`Subgroup.ext` `mul_one` `SubgroupClass.toInvMemClass` `Subgroup.instSubgroupClass`

QuotientAddGroup

Definitions

Name	Category	Theorems
`con` 📖	CompOp	6 math math: `AddCon.addSubgroup_quotientAddGroupCon`, `AddSubgroup.orderIsoAddCon_apply`, `con_ker_eq_addConKer`, `con_mono`, `con_le_iff`, `con_addSubgroup`
`liftEquiv` 📖	CompOp	2 math math: `liftEquiv_coe`, `liftEquiv_mk`
`map` 📖	CompOp	9 math math: `ker_map`, `map_comp_map`, `map_surjective_of_surjective`, `map_mk'`, `map_mk`, `map_id`, `map_map`, `quotientQuotientEquivQuotientAux_mk`, `map_id_apply`
`mk'` 📖	CompOp	35 math math: `AddSubgroup.IsSubnormal.quotient`, `mk'_eq_mk'`, `ker_map`, `coe_mk'`, `ker_mk'`, `CategoryTheory.ShortComplex.abLeftHomologyData_π`, `AddSubgroup.goursat_surjective`, `TopologicalAddGroup.IsSES.ofClosedAddSubgroup`, `ker_le_range_iff`, `mk'_comp_subtype`, `strictMono_comap_prod_map`, `AddSubgroup.Characteristic.comap_quotient_mk`, `comap_map_mk'`, `sound`, `Finset.card_nsmul_quotient_add_nsmul_inter_addSubgroup_le`, `ker_lift`, `lift_comp_mk'`, `quotient_norm_mk_eq`, `Finset.le_card_quotient_add_sq_inter_addSubgroup`, `AddCircle.continuous_mk'`, `comap_comap_center`, `map_mk'`, `addMonoidHom_ext_iff`, `range_mk'`, `map_normal`, `quotientQuotientEquivQuotientAux_mk`, `mk'_surjective`, `map_mk'_self`, `exists_norm_add_lt`, `AddSubgroup.focalAddSubgroupOf.mk'_addConj_eq`, `AddSubgroup.goursat`, `AddSubgroup.normedMk.apply`, `quotientQuotientEquivQuotientAux_mk_mk`, `mk'_apply`, `le_comap_mk'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addMonoidHom_ext` 📖	—	`AddMonoidHom.comp` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Quotient.addGroup` `mk'`	—	—	`AddMonoidHom.ext` `induction_on` `DFunLike.congr_fun`
`addMonoidHom_ext_iff` 📖	mathematical	—	`AddMonoidHom.comp` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Quotient.addGroup` `mk'`	—	`addMonoidHom_ext`
`coe_mk'` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Quotient.addGroup` `AddMonoidHom.instFunLike` `mk'`	—	—
`con_addSubgroup` 📖	mathematical	—	`con` `AddCon.addSubgroup` `instNormalAddSubgroup`	—	`AddCon.ext` `instNormalAddSubgroup` `con.eq_1` `leftRel_apply` `AddCon.mem_addSubgroup_iff` `add_zero` `add_neg_cancel_left` `AddCon.add` `AddCon.refl` `AddCon.symm` `neg_add_cancel`
`con_ker_eq_addConKer` 📖	mathematical	—	`con` `AddMonoidHom.ker` `AddMonoid.toAddZeroClass` `AddMonoidHom.normal_ker` `AddCon.ker` `AddMonoidHom` `AddZeroClass.toAddZero` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddZero.toAdd` `AddMonoidHom.instFunLike` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass`	—	`AddCon.ext` `AddMonoidHom.normal_ker` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `con.eq_1` `Setoid.comm'` `leftRel_apply` `AddCon.ker_rel` `AddMonoidHom.eq_iff`
`con_le_iff` 📖	mathematical	—	`AddCon` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCon.instLE` `con` `AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder`	—	`RelIso.map_rel_iff`
`con_mono` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder`	`AddCon` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCon.instLE` `con`	—	`con_le_iff`
`eq_iff_sub_mem` 📖	mathematical	—	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`eq` `AddSubgroup.Normal.mem_comm_iff` `sub_eq_add_neg`
`eq_zero_iff` 📖	mathematical	—	`HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Quotient.addGroup` `SetLike.instMembership` `AddSubgroup.instSetLike`	—	`eq` `add_zero` `AddSubgroup.neg_mem_iff`
`image_coe` 📖	mathematical	—	`Set.image` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `SetLike.coe` `AddSubgroup.instSetLike` `Set` `Set.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Quotient.addGroup`	—	`map_mk'_self`
`image_coe_inj` 📖	mathematical	—	`Set.image` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SetLike.coe` `AddSubgroup.instSetLike`	—	`preimage_image_coe` `Function.Surjective.preimage_injective` `mk_surjective`
`instNormalAddSubgroup` 📖	mathematical	—	`AddSubgroup.Normal` `AddCon.addSubgroup`	—	`AddCon.mem_addSubgroup_iff` `add_zero` `add_neg_cancel` `AddCon.add` `AddCon.refl`
`ker_le_range_iff` 📖	mathematical	—	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `AddMonoidHom.ker` `AddMonoidHom.range` `AddMonoidHom.comp` `SetLike.instMembership` `AddSubgroup.instSetLike` `HasQuotient.Quotient` `instHasQuotientAddSubgroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup.toAddGroup` `Quotient.addGroup` `mk'` `AddSubgroup.subtype` `AddMonoidHom` `instZeroAddMonoidHom`	—	`AddMonoidHom.ext` `eq_zero_iff` `DFunLike.congr_fun`
`ker_lift` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `AddMonoidHom.ker` `AddMonoid.toAddZeroClass`	`AddMonoidHom.ker` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `Quotient.addGroup` `AddMonoid.toAddZeroClass` `lift` `AddSubgroup.map` `mk'`	—	`lift_comp_mk'` `AddMonoidHom.comap_ker` `AddSubgroup.map_comap_eq_self_of_surjective` `mk'_surjective`
`ker_map` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `AddSubgroup.comap`	`AddMonoidHom.ker` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `Quotient.addGroup` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `map` `AddSubgroup.map` `mk'` `AddSubgroup.comap`	—	`ker_mk'` `ker_lift`
`ker_mk'` 📖	mathematical	—	`AddMonoidHom.ker` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Quotient.addGroup` `mk'`	—	`AddSubgroup.ext` `eq_zero_iff`
`leftRel_eq_top` 📖	mathematical	—	`leftRel` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Setoid.completeLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `AddSubgroup` `AddSubgroup.instTop`	—	`AddAction.mem_orbit_iff` `eq_neg_add_iff_add_eq` `AddSubgroup.mem_op` `AddOpposite.exists` `Setoid.mk_eq_top` `AddSubgroup.ext` `AddSubgroup.mem_top` `neg_zero` `zero_add`
`liftEquiv_coe` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `AddMonoidHom.ker`	`DFunLike.coe` `AddEquiv` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Quotient.addGroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `liftEquiv` `AddMonoidHom` `AddMonoidHom.instFunLike`	—	—
`liftEquiv_mk` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `AddMonoidHom.ker`	`DFunLike.coe` `AddEquiv` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Quotient.addGroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `liftEquiv` `AddMonoidHom` `AddMonoidHom.instFunLike`	—	—
`lift_comp_mk'` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `AddMonoidHom.ker` `AddMonoid.toAddZeroClass`	`AddMonoidHom.comp` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Quotient.addGroup` `lift` `mk'`	—	—
`lift_mk` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `AddMonoidHom.ker` `AddMonoid.toAddZeroClass`	`DFunLike.coe` `AddMonoidHom` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Quotient.addGroup` `AddMonoidHom.instFunLike` `lift`	—	—
`lift_mk'` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `AddMonoidHom.ker` `AddMonoid.toAddZeroClass`	`DFunLike.coe` `AddMonoidHom` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Quotient.addGroup` `AddMonoidHom.instFunLike` `lift`	—	—
`lift_quot_mk` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `AddMonoidHom.ker` `AddMonoid.toAddZeroClass`	`DFunLike.coe` `AddMonoidHom` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Quotient.addGroup` `AddMonoidHom.instFunLike` `lift` `leftRel`	—	—
`lift_surjective_of_surjective` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `AddMonoidHom.ker`	`HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Quotient.addGroup` `AddMonoidHom.instFunLike` `lift`	—	`Quotient.lift_surjective`
`map_comp_map` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `AddSubgroup.comap` `AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `LE.le.trans` `LE.le.trans_eq` `AddSubgroup.comap_mono` `AddSubgroup.comap_comap`	`AddMonoidHom.comp` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Quotient.addGroup` `map`	—	`AddMonoidHom.ext` `map_map`
`map_id` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `AddSubgroup.comap` `AddMonoidHom.id` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Eq.le` `AddSubgroup.comap_id`	`map` `AddMonoidHom.id` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `Quotient.addGroup`	—	`AddMonoidHom.ext` `map_id_apply`
`map_id_apply` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `AddSubgroup.comap` `AddMonoidHom.id` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Eq.le` `AddSubgroup.comap_id`	`DFunLike.coe` `AddMonoidHom` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Quotient.addGroup` `AddMonoidHom.instFunLike` `map` `AddMonoidHom.id`	—	`induction_on`
`map_map` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `AddSubgroup.comap` `AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `LE.le.trans` `LE.le.trans_eq` `AddSubgroup.comap_mono` `AddSubgroup.comap_comap`	`DFunLike.coe` `AddMonoidHom` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Quotient.addGroup` `AddMonoidHom.instFunLike` `map` `AddMonoidHom.comp`	—	`induction_on`
`map_mk` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `AddSubgroup.comap`	`DFunLike.coe` `AddMonoidHom` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Quotient.addGroup` `AddMonoidHom.instFunLike` `map`	—	—
`map_mk'` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `AddSubgroup.comap`	`DFunLike.coe` `AddMonoidHom` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Quotient.addGroup` `AddMonoidHom.instFunLike` `map` `mk'`	—	—
`map_mk'_self` 📖	mathematical	—	`AddSubgroup.map` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `Quotient.addGroup` `mk'` `Bot.bot` `AddSubgroup.instBot`	—	`AddSubgroup.ext` `AddSubgroup.mem_map` `AddSubgroup.mem_bot` `eq_zero_iff` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `AddSubgroup.instAddSubgroupClass`
`map_surjective_of_surjective` 📖	mathematical	`HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `AddSubgroup.comap`	`HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Quotient.addGroup` `AddMonoidHom.instFunLike` `map`	—	`lift_surjective_of_surjective`
`mk'_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Quotient.addGroup` `AddMonoidHom.instFunLike` `mk'`	—	—
`mk'_comp_subtype` 📖	mathematical	—	`AddMonoidHom.comp` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `HasQuotient.Quotient` `instHasQuotientAddSubgroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup.toAddGroup` `Quotient.addGroup` `mk'` `AddSubgroup.subtype` `AddMonoidHom` `instZeroAddMonoidHom`	—	`AddMonoidHom.ext` `eq_zero_iff` `SetLike.coe_mem`
`mk'_eq_mk'` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Quotient.addGroup` `AddMonoidHom.instFunLike` `mk'` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddZero.toAdd`	—	`eq` `eq_neg_add_iff_add_eq`
`mk'_surjective` 📖	mathematical	—	`HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Quotient.addGroup` `AddMonoidHom.instFunLike` `mk'`	—	`mk_surjective`
`mk_add` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `Quotient.addGroup`	—	—
`mk_neg` 📖	mathematical	—	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `Quotient.addGroup`	—	—
`mk_nsmul` 📖	mathematical	—	`AddMonoid.toNSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `Quotient.addGroup`	—	—
`mk_sub` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `Quotient.addGroup`	—	—
`mk_zero` 📖	mathematical	—	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `Quotient.addGroup`	—	—
`mk_zsmul` 📖	mathematical	—	`SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `Quotient.addGroup`	—	—
`nontrivial_iff` 📖	mathematical	—	`Nontrivial` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup`	—	`not_subsingleton_iff_nontrivial` `subsingleton_iff`
`preimage_image_coe` 📖	mathematical	—	`Set.preimage` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `Set.image` `Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SetLike.coe` `AddSubgroup.instSetLike`	—	`Set.ext` `eq_zero_iff` `sub_self` `sub_add_cancel` `right_eq_add` `AddRightCancelSemigroup.toIsRightCancelAdd`
`range_mk'` 📖	mathematical	—	`AddMonoidHom.range` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `Quotient.addGroup` `mk'` `Top.top` `AddSubgroup.instTop`	—	`AddMonoidHom.range_eq_top` `mk'_surjective`
`rightRel_eq_top` 📖	mathematical	—	`rightRel` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Setoid.completeLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `AddSubgroup` `AddSubgroup.instTop`	—	`AddAction.mem_orbit_iff` `eq_add_neg_iff_add_eq` `Setoid.mk_eq_top` `AddSubgroup.ext` `AddSubgroup.mem_top` `neg_zero` `add_zero`
`subsingleton_iff` 📖	mathematical	—	`HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup` `Top.top` `AddSubgroup.instTop`	—	`Quotient.subsingleton_iff` `leftRel_eq_top`

QuotientAddGroup.Quotient

Definitions

Name	Category	Theorems
`addCommGroup` 📖	CompOp	78 math math: `HurwitzZeta.isBigO_atTop_evenKernel_sub`, `HurwitzZeta.expZeta_zero`, `AddCircle.coe_eq_zero_iff`, `AddCircle.isAddQuotientCoveringMap_zsmul_of_ne_zero`, `CharacterModule.int.divByNat_self`, `AddCircle.card_torsion_le_of_isSMulRegular`, `AddCircle.coe_neg`, `AddCircle.isAddQuotientCoveringMap_nsmul_of_ne_zero`, `AddCircle.isAddQuotientCoveringMap_nsmul`, `QuotientAddGroup.equivIocMod_zero`, `HurwitzZeta.hurwitzZetaEven_zero`, `CharacterModule.instLinearMapClassIntAddCircleRatOfNat`, `AddCircle.finite_torsion_of_isSMulRegular`, `HurwitzZeta.completedSinZeta_neg`, `HurwitzZeta.evenKernel_eq_cosKernel_of_zero`, `HurwitzZeta.hurwitzZetaEven_apply_zero`, `HurwitzZeta.expZeta_one_sub`, `CategoryTheory.ShortComplex.abLeftHomologyData_π`, `fourier_neg'`, `HurwitzZeta.sinKernel_neg`, `HurwitzZeta.hurwitzEvenFEPair_zero_symm`, `AddCircle.equivAddCircle_apply_mk`, `HurwitzZeta.cosZeta_eq`, `AddAction.zmultiplesQuotientStabilizerEquiv_symm_apply`, `AddCircle.coe_eq_zero_iff_of_mem_Ico`, `quotient_norm_add_le`, `HurwitzZeta.completedHurwitzZetaEven_eq`, `HurwitzZeta.completedCosZeta₀_neg`, `fourier_eval_zero`, `AddCircle.coe_zero`, `HurwitzZeta.sinKernel_zero`, `HurwitzZeta.completedCosZeta₀_zero`, `HurwitzZeta.oddKernel_zero`, `QuotientAddGroup.nhds_zero_hasBasis`, `AddCircle.toCircle_zero`, `AddCircle.card_torsion_le_of_isSMulRegular_int`, `HurwitzZeta.completedHurwitzZetaOdd_neg`, `HurwitzZeta.oddKernel_neg`, `HurwitzZeta.evenKernel_neg`, `HurwitzZeta.cosZeta_zero`, `AddCircle.coe_eq_zero_of_pos_iff`, `HurwitzZeta.completedHurwitzZetaEven_zero`, `HurwitzZeta.hurwitzZetaOdd_eq`, `HurwitzZeta.hurwitzZeta_zero`, `QuotientAddGroup.mk_sum`, `QuotientAddGroup.zmultiples_zsmul_eq_zsmul_iff`, `HurwitzZeta.hurwitzZeta_one_sub`, `HurwitzZeta.completedHurwitzZetaEven₀_neg`, `HurwitzZeta.completedHurwitzZetaEven₀_zero`, `HurwitzZeta.sinZeta_neg`, `HurwitzZeta.completedCosZeta_eq`, `HurwitzZeta.hurwitzEvenFEPair_neg`, `AddCircle.finite_torsion`, `HurwitzZeta.completedHurwitzZetaEven_neg`, `QuotientAddGroup.zmultiples_nsmul_eq_nsmul_iff`, `HurwitzZeta.cosKernel_neg`, `CharacterModule.uncurry_apply`, `AddCircle.nsmul_eq_zero_iff`, `fourier_zero'`, `AddCircle.isAddQuotientCoveringMap_zsmul`, `AddCircle.coe_period`, `AddCircle.finite_torsion_of_isSMulRegular_int`, `HurwitzZeta.completedCosZeta_zero`, `HurwitzZeta.completedCosZeta_neg`, `HurwitzZeta.cosZeta_neg`, `QuotientAddGroup.equivIcoMod_zero`, `HurwitzZeta.hurwitzZetaOdd_neg`, `ZMod.toAddCircle_eq_zero`, `HurwitzZeta.completedHurwitzZetaEven_residue_zero`, `HurwitzZeta.sinZeta_eq`, `AddCircle.coe_add`, `CharacterModule.homEquiv_apply_apply`, `AddCircle.equivAddCircle_symm_apply_mk`, `AddCircle.toCircle_neg`, `HurwitzZeta.hurwitzZetaEven_neg`, `HurwitzZeta.hurwitzZetaEven_eq`, `HurwitzKernelBounds.isBigO_atTop_F_int_zero_sub`, `HurwitzZeta.hasSum_int_evenKernel₀`
`addGroup` 📖	CompOp	153 math math: `QuotientAddGroup.kerLift_mk`, `AddCircle.not_isOfFinAddOrder_iff_forall_rat_ne_div`, `AddCircle.exists_gcd_eq_one_of_isOfFinAddOrder`, `AddSubgroup.IsSubnormal.quotient`, `AddCircle.isAddQuotientCoveringMap_zsmul_of_ne_zero`, `ZMod.LFunction_stdAddChar_eq_expZeta`, `QuotientAddGroup.completeSpace_right'`, `AddSubgroup.Normal.quotient_commutative_iff_addCommutator_le`, `AddCircle.card_torsion_le_of_isSMulRegular`, `QuotientAddGroup.addEquivPiModRangeNSMulAddMonoidHom_apply`, `QuotientAddGroup.equivQuotientZSMulOfEquiv_symm`, `AddCircle.isAddFundamentalDomain_of_ae_ball`, `QuotientAddGroup.mk'_eq_mk'`, `AddCircle.isAddQuotientCoveringMap_nsmul_of_ne_zero`, `QuotientAddGroup.ker_map`, `AddCircle.isAddQuotientCoveringMap_nsmul`, `QuotientAddGroup.coe_mk'`, `QuotientAddGroup.completeSpace_left`, `ZMod.completedLFunction_def_even`, `MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addInvariantMeasure_quotient`, `QuotientAddGroup.liftEquiv_coe`, `CharacterModule.curry_apply_apply`, `AddCircle.coe_zsmul`, `QuotientAddGroup.ker_mk'`, `AddCircle.isOfFinAddOrder_iff_exists_rat_eq_div`, `AdjoinRoot.evalEval_apply`, `AddCircle.finite_torsion_of_isSMulRegular`, `ZMod.LFunction_def_odd`, `AddCircle.instIsAddHaarMeasureRealVolume`, `QuotientAddGroup.equivQuotientZSMulOfEquiv_trans`, `AddCircle.dense_addSubgroup_iff_ne_zmultiples`, `QuotientAddGroup.completeSpace_right`, `AddCircle.denseRange_zsmul_iff`, `QuotientAddGroup.liftEquiv_mk`, `fourier_neg'`, `ZMod.toAddCircle_inj`, `ZMod.completedLFunction_def_odd`, `AddGroup.exponent_quotient_dvd`, `AddCircle.addOrderOf_div_of_gcd_eq_one`, `AddCircle.coe_sub`, `AddSubgroup.goursat_surjective`, `TopologicalAddGroup.IsSES.ofClosedAddSubgroup`, `QuotientAddGroup.lift_mk'`, `AddCircle.finite_setOf_addOrderOf_eq`, `AddAction.zmultiplesQuotientStabilizerEquiv_symm_apply`, `QuotientAddGroup.map_comp_map`, `QuotientAddGroup.instIsTopologicalAddGroup`, `QuotientAddGroup.fg`, `QuotientAddGroup.ker_le_range_iff`, `QuotientAddGroup.mk'_comp_subtype`, `AddCircle.coe_nsmul`, `QuotientAddGroup.strictMono_comap_prod_map`, `AddCircle.card_addOrderOf_eq_totient`, `QuotientAddGroup.mk_add`, `AddSubgroup.Characteristic.comap_quotient_mk`, `QuotientAddGroup.comap_map_mk'`, `QuotientAddGroup.sound`, `Finset.card_nsmul_quotient_add_nsmul_inter_addSubgroup_le`, `QuotientAddGroup.homQuotientZSMulOfHom_comp_of_rightInverse`, `ZMod.toAddCircle_natCast`, `QuotientAddGroup.quotientAddEquivOfEq_mk`, `QuotientAddGroup.ker_lift`, `AddCircle.toCircle_zsmul`, `AddCircle.card_torsion_le_of_isSMulRegular_int`, `QuotientAddGroup.lift_comp_mk'`, `QuotientAddGroup.lift_mk`, `UnitAddCircle.mem_approxAddOrderOf_iff`, `QuotientAddGroup.mk_sub`, `QuotientAddGroup.quotientKerEquivOfRightInverse_symm_apply`, `ZMod.LFunction_def_even`, `fourier_apply`, `quotient_norm_mk_eq`, `CharacterModule.homEquiv_symm_apply_apply_apply`, `QuotientAddGroup.quotientMapAddSubgroupOfOfLe_mk`, `QuotientAddGroup.mk_nat_mul`, `AddCircle.denseRange_zsmul_coe_iff`, `QuotientAddGroup.norm_lift_apply_le`, `QuotientAddGroup.map_surjective_of_surjective`, `QuotientAddGroup.mk_zero`, `QuotientAddGroup.quotientBot_apply`, `AddCircle.ergodic_zsmul`, `QuotientAddGroup.quotientKerEquivOfRightInverse_apply`, `Finset.le_card_quotient_add_sq_inter_addSubgroup`, `AddCommGroup.isTorsion_quotient_range_nsmulAddMonoidHom`, `QuotientAddGroup.mk_zsmul`, `QuotientAddGroup.mk_nsmul`, `QuotientAddGroup.image_coe`, `ZMod.toAddCircle_intCast`, `AddCircle.continuous_mk'`, `ZMod.toAddCircle_apply`, `QuotientAddGroup.comap_comap_center`, `QuotientAddGroup.map_mk'`, `QuotientAddGroup.zmultiples_zsmul_eq_zsmul_iff`, `ZMod.toAddCircle_injective`, `AddCircle.addOrderOf_eq_pos_iff`, `QuotientAddGroup.quotientBot_symm_apply`, `QuotientAddGroup.addMonoidHom_ext_iff`, `QuotientAddGroup.range_mk'`, `AddCircle.finite_torsion`, `QuotientAddGroup.map_mk`, `QuotientAddGroup.lift_surjective_of_surjective`, `QuotientAddGroup.equivQuotientZSMulOfEquiv_refl`, `QuotientAddGroup.zmultiples_nsmul_eq_nsmul_iff`, `QuotientAddGroup.norm_eq_addGroupSeminorm`, `AddCircle.nsmul_eq_zero_iff`, `AddCircle.isAddQuotientCoveringMap_zsmul`, `UnitAddCircle.mem_addWellApproximable_iff`, `QuotientAddGroup.map_normal`, `QuotientAddGroup.map_id`, `AddCircle.finite_torsion_of_isSMulRegular_int`, `QuotientAddGroup.map_map`, `QuotientAddGroup.lift_quot_mk`, `AddSubgroup.instIsAddCommutativeQuotientSubtypeMemFocalAddSubgroupOf`, `AddCircle.addOrderOf_period_div`, `AddAction.stabilizer_image_coe_quotient`, `QuotientAddGroup.kerLift_mk'`, `fourier_coe_apply'`, `QuotientAddGroup.quotientQuotientEquivQuotientAux_mk`, `QuotientAddGroup.eq_zero_iff`, `AddCircle.addOrderOf_div_of_gcd_eq_one'`, `QuotientAddGroup.mk_int_mul`, `QuotientAddGroup.mk'_surjective`, `QuotientAddGroup.kerLift_injective`, `QuotientAddGroup.mk_neg`, `ZMod.toAddCircle_eq_zero`, `QuotientAddGroup.map_mk'_self`, `QuotientAddGroup.exists_norm_add_lt`, `AddCircle.intCast_div_mul_eq_zsmul`, `fourier_add'`, `AddSubgroup.focalAddSubgroupOf.mk'_addConj_eq`, `AddCircle.addOrderOf_coe_rat`, `MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addHaarMeasure_quotient`, `AddSubgroup.goursat`, `AddSubgroup.normedMk.apply`, `instIsAddHaarMeasureUnitAddCircleVolume`, `ZMod.LFunction_dft`, `CharacterModule.dual_apply`, `QuotientAddGroup.rangeKerLift_injective`, `KaehlerDifferential.quotKerTotalEquiv_apply`, `QuotientAddGroup.instIsAddTorsionFree`, `QuotientAddGroup.rangeKerLift_surjective`, `QuotientAddGroup.quotientQuotientEquivQuotientAux_mk_mk`, `QuotientAddGroup.mk'_apply`, `QuotientAddGroup.homQuotientZSMulOfHom_comp`, `QuotientAddGroup.completeSpace_left'`, `AddCircle.ergodic_zsmul_add`, `AddCircle.gcd_mul_addOrderOf_div_eq`, `QuotientAddGroup.homQuotientZSMulOfHom_id`, `QuotientAddGroup.le_comap_mk'`, `Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply`, `AddCircle.natCast_div_mul_eq_nsmul`, `IsFundamentalDomain.AddQuotientMeasureEqMeasurePreimage_vaddAddHaarMeasure`, `QuotientAddGroup.map_id_apply`

QuotientGroup

Definitions

Name	Category	Theorems
`con` 📖	CompOp	6 math math: `con_le_iff`, `con_subgroup`, `Subgroup.orderIsoCon_apply`, `con_ker_eq_conKer`, `Con.subgroup_quotientGroupCon`, `con_mono`
`liftEquiv` 📖	CompOp	2 math math: `liftEquiv_coe`, `liftEquiv_mk`
`map` 📖	CompOp	10 math math: `quotientQuotientEquivQuotientAux_mk`, `Ideal.Quotient.stabilizerHomSurjectiveAuxFunctor_aux`, `map_id`, `map_surjective_of_surjective`, `map_mk'`, `map_mk`, `ker_map`, `map_id_apply`, `map_comp_map`, `map_map`
`mk'` 📖	CompOp	47 math math: `groupHomology.map₁_quotientGroupMk'_epi`, `groupHomology.coinfNatTrans_app`, `coe_mk'`, `IsGaloisGroup.quotientMap`, `groupCohomology.infNatTrans_app`, `Subgroup.IsSubnormal.quotient`, `quotientQuotientEquivQuotientAux_mk`, `lift_comp_mk'`, `groupHomology.H1CoresCoinf_g`, `TopologicalGroup.IsSES.ofClosedSubgroup`, `mk'_apply`, `mk'_comp_subtype`, `mk'_eq_mk'`, `map_mk'`, `ker_map`, `quotientQuotientEquivQuotientAux_mk_mk`, `congr_apply`, `range_mk'`, `ker_lift`, `comap_upperCentralSeries_quotient_center`, `map_normal`, `Finset.le_card_quotient_mul_sq_inter_subgroup`, `congr_mk'`, `Subgroup.goursat_surjective`, `exists_norm_mul_lt`, `comap_map_mk'`, `Finset.card_pow_quotient_mul_pow_inter_subgroup_le`, `groupHomology.H1CoresCoinfOfTrivial_g`, `Subgroup.focalSubgroupOf.mk'_conj_eq`, `monoidHom_ext_iff`, `upperCentralSeriesStep_eq_comap_center`, `map_mk'_self`, `ClassGroup.equiv_mk0`, `ker_le_range_iff`, `mk'_surjective`, `comap_comap_center`, `ker_mk'`, `strictMono_comap_prod_map`, `groupCohomology.H1InfRes_f`, `le_comap_mk'`, `ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk`, `Subgroup.Characteristic.comap_quotient_mk`, `ClassGroup.mk_def`, `sound`, `groupHomology.mapCycles₁_quotientGroupMk'_epi`, `Subgroup.goursat`, `ClassGroup.equiv_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mk'` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.group` `MonoidHom.instFunLike` `mk'`	—	—
`con_ker_eq_conKer` 📖	mathematical	—	`con` `MonoidHom.ker` `Monoid.toMulOneClass` `MonoidHom.normal_ker` `Con.ker` `MonoidHom` `MulOneClass.toMulOne` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulOne.toMul` `MonoidHom.instFunLike` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass`	—	`Con.ext` `MonoidHom.normal_ker` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `con.eq_1` `Setoid.comm'` `leftRel_apply` `Con.ker_rel` `MonoidHom.eq_iff`
`con_le_iff` 📖	mathematical	—	`Con` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Con.instLE` `con` `Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder`	—	`RelIso.map_rel_iff`
`con_mono` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder`	`Con` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Con.instLE` `con`	—	`con_le_iff`
`con_subgroup` 📖	mathematical	—	`con` `Con.subgroup` `instNormalSubgroup`	—	`Con.ext` `instNormalSubgroup` `con.eq_1` `leftRel_apply` `Con.mem_subgroup_iff` `mul_one` `mul_inv_cancel_left` `Con.mul` `Con.refl` `Con.symm` `inv_mul_cancel`
`congr_apply` 📖	mathematical	`Subgroup.map` `MonoidHomClass.toMonoidHom` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass`	`DFunLike.coe` `MulEquiv` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.group` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `congr` `MonoidHom` `MonoidHom.instFunLike` `mk'`	—	`MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass`
`congr_mk` 📖	mathematical	`Subgroup.map` `MonoidHomClass.toMonoidHom` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass`	`DFunLike.coe` `MulEquiv` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.group` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `congr`	—	`MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass`
`congr_mk'` 📖	mathematical	`Subgroup.map` `MonoidHomClass.toMonoidHom` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass`	`DFunLike.coe` `MulEquiv` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.group` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `congr` `MonoidHom` `MonoidHom.instFunLike` `mk'`	—	`MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass`
`congr_refl` 📖	mathematical	`Subgroup` `Subgroup.map` `MonoidHomClass.toMonoidHom` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `MulEquiv.refl` `Subgroup.map_id`	`congr` `MulEquiv.refl` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `Quotient.group`	—	`MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `MulEquiv.ext`
`congr_symm` 📖	mathematical	`Subgroup.map` `MonoidHomClass.toMonoidHom` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass`	`MulEquiv.symm` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.group` `congr` `Subgroup.map` `MonoidHomClass.toMonoidHom` `MulEquiv` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `Subgroup.map_symm_eq_iff_map_eq`	—	`MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass`
`eq_iff_div_mem` 📖	mathematical	—	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`eq` `Subgroup.Normal.mem_comm_iff` `div_eq_mul_inv`
`eq_one_iff` 📖	mathematical	—	`HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Quotient.group` `SetLike.instMembership` `Subgroup.instSetLike`	—	`eq` `mul_one` `Subgroup.inv_mem_iff`
`image_coe` 📖	mathematical	—	`Set.image` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `SetLike.coe` `Subgroup.instSetLike` `Set` `Set.one` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Quotient.group`	—	`map_mk'_self`
`image_coe_inj` 📖	mathematical	—	`Set.image` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.coe` `Subgroup.instSetLike`	—	`Function.Surjective.preimage_injective` `mk_surjective`
`instNormalSubgroup` 📖	mathematical	—	`Subgroup.Normal` `Con.subgroup`	—	`mul_one` `mul_inv_cancel` `Con.mul` `Con.refl`
`ker_le_range_iff` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `MonoidHom.ker` `MonoidHom.range` `MonoidHom.comp` `SetLike.instMembership` `Subgroup.instSetLike` `HasQuotient.Quotient` `instHasQuotientSubgroup` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `Quotient.group` `mk'` `Subgroup.subtype` `MonoidHom` `instOneMonoidHom`	—	`MonoidHom.ext` `eq_one_iff` `DFunLike.congr_fun`
`ker_lift` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `MonoidHom.ker` `Monoid.toMulOneClass`	`MonoidHom.ker` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `Quotient.group` `Monoid.toMulOneClass` `lift` `Subgroup.map` `mk'`	—	`lift_comp_mk'` `MonoidHom.comap_ker` `Subgroup.map_comap_eq_self_of_surjective` `mk'_surjective`
`ker_map` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.comap`	`MonoidHom.ker` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `Quotient.group` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `map` `Subgroup.map` `mk'` `Subgroup.comap`	—	`ker_mk'` `ker_lift`
`ker_mk'` 📖	mathematical	—	`MonoidHom.ker` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.group` `mk'`	—	`Subgroup.ext` `eq_one_iff`
`leftRel_eq_top` 📖	mathematical	—	`leftRel` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Setoid.completeLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Subgroup` `Subgroup.instTop`	—	`Subgroup.ext` `inv_one` `one_mul`
`liftEquiv_coe` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `MonoidHom.ker`	`DFunLike.coe` `MulEquiv` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.group` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `liftEquiv` `MonoidHom` `MonoidHom.instFunLike`	—	—
`liftEquiv_mk` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `MonoidHom.ker`	`DFunLike.coe` `MulEquiv` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.group` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `liftEquiv` `MonoidHom` `MonoidHom.instFunLike`	—	—
`lift_comp_mk'` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `MonoidHom.ker` `Monoid.toMulOneClass`	`MonoidHom.comp` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.group` `lift` `mk'`	—	—
`lift_mk` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `MonoidHom.ker` `Monoid.toMulOneClass`	`DFunLike.coe` `MonoidHom` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.group` `MonoidHom.instFunLike` `lift`	—	—
`lift_mk'` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `MonoidHom.ker` `Monoid.toMulOneClass`	`DFunLike.coe` `MonoidHom` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.group` `MonoidHom.instFunLike` `lift`	—	—
`lift_quot_mk` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `MonoidHom.ker` `Monoid.toMulOneClass`	`DFunLike.coe` `MonoidHom` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.group` `MonoidHom.instFunLike` `lift` `leftRel`	—	—
`lift_surjective_of_surjective` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `MonoidHom.ker`	`HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.group` `MonoidHom.instFunLike` `lift`	—	`Quotient.lift_surjective`
`map_comp_map` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.comap` `MonoidHom.comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LE.le.trans` `LE.le.trans_eq` `Subgroup.comap_mono` `Subgroup.comap_comap`	`MonoidHom.comp` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.group` `map`	—	`MonoidHom.ext` `map_map`
`map_id` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.comap` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Eq.le` `Subgroup.comap_id`	`map` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `Quotient.group`	—	`MonoidHom.ext` `map_id_apply`
`map_id_apply` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.comap` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Eq.le` `Subgroup.comap_id`	`DFunLike.coe` `MonoidHom` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.group` `MonoidHom.instFunLike` `map` `MonoidHom.id`	—	`induction_on`
`map_map` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.comap` `MonoidHom.comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LE.le.trans` `LE.le.trans_eq` `Subgroup.comap_mono` `Subgroup.comap_comap`	`DFunLike.coe` `MonoidHom` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.group` `MonoidHom.instFunLike` `map` `MonoidHom.comp`	—	`induction_on`
`map_mk` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.comap`	`DFunLike.coe` `MonoidHom` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.group` `MonoidHom.instFunLike` `map`	—	—
`map_mk'` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.comap`	`DFunLike.coe` `MonoidHom` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.group` `MonoidHom.instFunLike` `map` `mk'`	—	—
`map_mk'_self` 📖	mathematical	—	`Subgroup.map` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `Quotient.group` `mk'` `Bot.bot` `Subgroup.instBot`	—	`Subgroup.ext` `OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass`
`map_surjective_of_surjective` 📖	mathematical	`HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.comap`	`HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.group` `MonoidHom.instFunLike` `map`	—	`lift_surjective_of_surjective`
`mk'_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.group` `MonoidHom.instFunLike` `mk'`	—	—
`mk'_comp_subtype` 📖	mathematical	—	`MonoidHom.comp` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `HasQuotient.Quotient` `instHasQuotientSubgroup` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `Quotient.group` `mk'` `Subgroup.subtype` `MonoidHom` `instOneMonoidHom`	—	`MonoidHom.ext`
`mk'_eq_mk'` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.group` `MonoidHom.instFunLike` `mk'` `SetLike.instMembership` `Subgroup.instSetLike` `MulOne.toMul`	—	`eq`
`mk'_surjective` 📖	mathematical	—	`HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.group` `MonoidHom.instFunLike` `mk'`	—	`mk_surjective`
`mk_div` 📖	mathematical	—	`DivInvMonoid.toDiv` `Group.toDivInvMonoid` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `Quotient.group`	—	—
`mk_inv` 📖	mathematical	—	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `Quotient.group`	—	—
`mk_mul` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `Quotient.group`	—	—
`mk_one` 📖	mathematical	—	`InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `Quotient.group`	—	—
`mk_pow` 📖	mathematical	—	`Monoid.toPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `Quotient.group`	—	—
`mk_zpow` 📖	mathematical	—	`DivInvMonoid.toZPow` `Group.toDivInvMonoid` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `Quotient.group`	—	—
`monoidHom_ext` 📖	—	`MonoidHom.comp` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.group` `mk'`	—	—	`MonoidHom.ext` `induction_on` `DFunLike.congr_fun`
`monoidHom_ext_iff` 📖	mathematical	—	`MonoidHom.comp` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Quotient.group` `mk'`	—	`monoidHom_ext`
`nontrivial_iff` 📖	mathematical	—	`Nontrivial` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup`	—	—
`preimage_image_coe` 📖	mathematical	—	`Set.preimage` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `Set.image` `Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.coe` `Subgroup.instSetLike`	—	`Set.ext` `eq_one_iff` `div_self'` `div_mul_cancel` `RightCancelSemigroup.toIsRightCancelMul`
`range_mk'` 📖	mathematical	—	`MonoidHom.range` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `Quotient.group` `mk'` `Top.top` `Subgroup.instTop`	—	`MonoidHom.range_eq_top` `mk'_surjective`
`rightRel_eq_top` 📖	mathematical	—	`rightRel` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Setoid.completeLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Subgroup` `Subgroup.instTop`	—	`Subgroup.ext` `inv_one` `mul_one`
`subsingleton_iff` 📖	mathematical	—	`HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup` `Top.top` `Subgroup.instTop`	—	—

QuotientGroup.Quotient

Definitions

Name	Category	Theorems
`commGroup` 📖	CompOp	8 math math: `NumberField.Units.fun_eq_repr`, `QuotientGroup.nhds_one_hasBasis`, `NumberField.Units.fundSystem_mk`, `NumberField.Units.rank_modTorsion`, `NumberField.Units.logEmbeddingEquiv_apply`, `NumberField.Units.instFiniteIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion`, `QuotientGroup.mk_prod`, `NumberField.Units.instFreeIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion`
`group` 📖	CompOp	152 math math: `QuotientGroup.homQuotientZPowOfHom_id`, `QuotientGroup.mk_one`, `groupHomology.map₁_quotientGroupMk'_epi`, `QuotientGroup.kerLift_mk`, `QuotientGroup.lift_mk`, `groupHomology.coinfNatTrans_app`, `QuotientGroup.coe_mk'`, `MonoidHom.restrictHomKerEquiv_apply_coe`, `nilpotencyClass_quotient_center`, `Subgroup.focalSubgroupOf.pow_index_surjective`, `QuotientGroup.rangeKerLift_injective`, `InfiniteGalois.normalAutEquivQuotient_apply`, `Subgroup.transferFocal_surjective`, `QuotientGroup.completeSpace_left`, `MulAction.quotient_out_smul_fixedPoints`, `groupHomology.H1CoresCoinf_X₃`, `QuotientGroup.kerLift_mk'`, `Subgroup.Normal.quotient_commutative_iff_commutator_le`, `IsGaloisGroup.quotientMap`, `QuotientGroup.liftEquiv_coe`, `IsPGroup.to_quotient`, `MeasureTheory.QuotientMeasureEqMeasurePreimage.mulInvariantMeasure_quotient`, `QuotientGroup.completeSpace_right`, `QuotientGroup.quotientKerEquivOfRightInverse_apply`, `MeasureTheory.QuotientMeasureEqMeasurePreimage.haarMeasure_quotient`, `NumberField.Units.logEmbeddingQuot_apply`, `QuotientGroup.completeSpace_right'`, `QuotientGroup.liftEquiv_mk`, `QuotientGroup.congr_refl`, `groupCohomology.infNatTrans_app`, `IsGaloisGroup.quotient`, `IsDedekindDomain.selmerGroup.monotone`, `QuotientGroup.congr_symm`, `Subgroup.IsSubnormal.quotient`, `QuotientGroup.instIsMulTorsionFree`, `Representation.ofQuotient_coe_apply`, `MonoidHom.restrictHomKerEquiv_symm_coe_apply`, `QuotientGroup.quotientQuotientEquivQuotientAux_mk`, `QuotientGroup.lift_comp_mk'`, `groupHomology.H1CoresCoinf_g`, `TopologicalGroup.IsSES.ofClosedSubgroup`, `QuotientGroup.mk'_apply`, `IsGalois.normalAutEquivQuotient_apply`, `QuotientGroup.rangeKerLift_surjective`, `QuotientGroup.quotientKerEquivOfRightInverse_symm_apply`, `QuotientGroup.mulEquivPiModRangePowMonoidHom_apply`, `Ideal.Quotient.stabilizerHomSurjectiveAuxFunctor_aux`, `QuotientGroup.map_id`, `QuotientGroup.map_surjective_of_surjective`, `MulAction.coe_quotient_smul_fixedPoints`, `QuotientGroup.mk'_comp_subtype`, `QuotientGroup.mk'_eq_mk'`, `QuotientGroup.map_mk'`, `QuotientGroup.map_mk`, `QuotientGroup.quotientMapSubgroupOfOfLe_mk`, `IsPGroup.cyclic_center_quotient_of_card_eq_prime_sq`, `QuotientGroup.ker_map`, `Ideal.Quotient.stabilizerQuotientInertiaEquiv_mk`, `QuotientGroup.lift_mk'`, `QuotientGroup.kerLift_injective`, `instIsInvariantSubtypeMemSubalgebraSubalgebraSubgroupQuotient`, `Action.FintypeCat.quotientToEndHom_mk`, `QuotientGroup.quotientQuotientEquivQuotientAux_mk_mk`, `QuotientGroup.congr_apply`, `QuotientGroup.mk_pow`, `Submodule.unitsQuotEquivRelPic_symm_apply`, `QuotientGroup.range_mk'`, `QuotientGroup.homQuotientZPowOfHom_comp_of_rightInverse`, `QuotientGroup.ker_lift`, `comap_upperCentralSeries_quotient_center`, `QuotientGroup.fg`, `QuotientGroup.map_normal`, `QuotientGroup.homQuotientZPowOfHom_comp`, `groupCohomology.H1InfRes_X₁`, `QuotientGroup.completeSpace_left'`, `QuotientGroup.lift_surjective_of_surjective`, `ClassGroup.equivPic_symm_apply`, `Finset.le_card_quotient_mul_sq_inter_subgroup`, `QuotientGroup.congr_mk'`, `QuotientGroup.mk_inv`, `Subgroup.instIsMulCommutativeQuotientSubtypeMemFocalSubgroupOf`, `MulAction.zpowersQuotientStabilizerEquiv_symm_apply`, `IsDedekindDomain.selmerGroup.fromUnit_ker`, `MulAction.stabilizer_image_coe_quotient`, `Subgroup.goursat_surjective`, `solvable_quotient_of_solvable`, `QuotientGroup.exists_norm_mul_lt`, `QuotientGroup.equivQuotientZPowOfEquiv_trans`, `QuotientGroup.comap_map_mk'`, `Subgroup.transferFocal_eq_pow`, `ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply`, `IsDedekindDomain.selmerGroup.fromUnitLift_injective`, `NumberField.Units.logEmbeddingQuot_injective`, `QuotientGroup.map_id_apply`, `IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_smulHaarMeasure`, `Finset.card_pow_quotient_mul_pow_inter_subgroup_le`, `nilpotencyClass_quotient_le`, `groupHomology.H1CoresCoinfOfTrivial_g`, `QuotientGroup.map_comp_map`, `Rep.quotientToCoinvariantsFunctor_map_hom_toLinearMap`, `CommGroup.isTorsion_quotient_range_powMonoidHom`, `Subgroup.ker_restrict_transferFocal_eq_focalSubgroupOf`, `Subgroup.focalSubgroupOf.mk'_conj_eq`, `Subgroup.ker_transferFocal_inf_eq_focalSubgroup`, `QuotientGroup.mk_zpow`, `Subgroup.IsComplement'.QuotientMulEquiv_symm_apply`, `QuotientGroup.monoidHom_ext_iff`, `QuotientGroup.quotientBot_apply`, `QuotientGroup.congr_mk`, `upperCentralSeriesStep_eq_comap_center`, `nilpotencyClass_eq_quotient_center_plus_one`, `QuotientGroup.map_mk'_self`, `ClassGroup.equiv_mk0`, `groupHomology.H1CoresCoinfOfTrivial_X₃`, `QuotientGroup.ker_le_range_iff`, `QuotientGroup.mk'_surjective`, `QuotientGroup.equivQuotientZPowOfEquiv_refl`, `QuotientGroup.mk_mul`, `QuotientGroup.image_coe`, `QuotientGroup.norm_eq_groupSeminorm`, `Subgroup.IsComplement'.QuotientMulEquiv_apply`, `QuotientGroup.equivQuotientZPowOfEquiv_symm`, `QuotientGroup.comap_comap_center`, `QuotientGroup.map_map`, `ClassGroup.equivPic_apply`, `IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_mod_eq`, `QuotientGroup.instIsTopologicalGroup`, `QuotientGroup.ker_mk'`, `QuotientGroup.eq_one_iff`, `QuotientGroup.lift_quot_mk`, `Subgroup.commProb_quotient_le`, `QuotientGroup.strictMono_comap_prod_map`, `groupCohomology.H1InfRes_f`, `QuotientGroup.quotientBot_symm_apply`, `QuotientGroup.mk_div`, `QuotientGroup.le_comap_mk'`, `nilpotent_quotient_of_nilpotent`, `ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk`, `instSMulCommClassQuotientSubgroupSubtypeMemSubalgebraSubalgebra`, `Subgroup.Characteristic.comap_quotient_mk`, `ClassGroup.mk_def`, `QuotientGroup.sound`, `groupHomology.mapCycles₁_quotientGroupMk'_epi`, `IsZGroup.instQuotientSubgroupOfFinite`, `Subgroup.goursat`, `ClassGroup.equiv_mk`, `IsDedekindDomain.selmerGroup.valuation_ker_eq`, `Group.IsPerfect.instQuotientSubgroup`, `Group.exponent_quotient_dvd`, `Submodule.unitsQuotEquivRelPic_apply_coe`, `QuotientGroup.quotientMulEquivOfEq_mk`, `Rep.quotientToCoinvariantsFunctor_obj_V`

Subgroup

Definitions

Name	Category	Theorems
`orderIsoCon` 📖	CompOp	2 math math: `orderIsoCon_apply`, `orderIsoCon_symm_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`orderIsoCon_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Subgroup` `Normal` `Con` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Con.instLE` `RelIso.instFunLike` `orderIsoCon` `QuotientGroup.con`	—	—
`orderIsoCon_symm_apply_coe` 📖	mathematical	—	`Subgroup` `Normal` `DFunLike.coe` `RelIso` `Con` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Con.instLE` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `RelIso.instFunLike` `RelIso.symm` `orderIsoCon` `Con.subgroup`	—	—

---

← Back to Index