Subgroup 📖 | CompData | 1874 mathmath: Subgroup.card_map_of_injective, MulAction.Quotient.coe_smul_out, IsPGroup.center_nontrivial, CongruenceSubgroup.Gamma_zero_bot, fixingSubgroup_union, SubMulAction.ofStabilizer.isPretransitive_iff_of_conj, Submonoid.units_iInf, DoubleCoset.doubleCoset_union_rightCoset, GrpCat.SurjectiveOfEpiAuxs.τ_apply_fromCoset, Sylow.isPGroup', Subgroup.mem_centralizer_iff_commutator_eq_one, Subgroup.mulSingle_mem_pi, MulAction.isPreprimitive_of_fixingSubgroup_empty_iff, QuotientGroup.homQuotientZPowOfHom_id, Subgroup.smul_mem_pointwise_smul_iff₀, MonoidHom.comap_bot, Subgroup.instFiniteSubtypeMem, Subgroup.card_eq_card_quotient_mul_card_subgroup, SubMulAction.ofStabilizer.conjMap_comp_apply, ConjAct.fixedPoints_eq_center, ModularGroup.SLOnGLPos_smul_apply, fixingSubgroup_antitone, MulAction.IwasawaStructure.commutator_le, Subgroup.pointwise_smul_le_pointwise_smul_iff, MonoidWithZeroHom.mem_valueGroup, Subgroup.characteristic_centralizer, mem_rootsOfUnity, Matrix.GLPos.coe_neg_apply, Subgroup.sup_eq_closure_mul, QuotientGroup.mk_one, Subgroup.ofUnits_bot, ValuationSubring.coe_mem_principalUnitGroup_iff, Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_apply, Subgroup.adjoinNegOne_eq_self_iff, Subgroup.isComplement'_top_left, QuotientGroup.isQuotientMap_mk, Subgroup.exists_mem_sup, Subgroup.mem_normalizer_iff'', Subgroup.closure_eq, Subgroup.quotientEquivOfEq_mk, mem_zpowers_iff_mem_range_orderOf, Ideal.Quotient.map_ker_stabilizer_subtype, Subgroup.prod_subgroupOf_prod_normal, Subgroup.equivSMul_apply_coe, QuotientGroup.norm_mk, QuotientGroup.image_coe_inj, Subgroup.gc_map_comap, groupHomology.map₁_quotientGroupMk'_epi, MulAction.IwasawaStructure.is_generator, QuotientGroup.kerLift_mk, zpowers_eq_top_of_prime_card, Subgroup.unop_inf, Fintype.card_coeSort_range, IsPGroup.card_center_eq_prime_pow, groupHomology.coinfNatTrans_app, IsCyclic.isComplement', Subgroup.coe_pointwise_smul, Subgroup.centerCongr_symm_apply_coe, modularCyclotomicCharacter.id, rootsOfUnityEquivOfPrimitiveRoots_apply_coe_inv_val, alternatingGroup.eq_bot_of_card_le_two, IsOfFinOrder.mem_powers_iff_mem_zpowers, NumberField.IsCMField.zpowers_complexConj_eq_top, Subgroup.inf_relIndex_left, Subgroup.toSubmonoid_le, NumberField.Units.instNonemptySubtypeUnitsRingOfIntegersMemSubgroupTorsion, QuotientGroup.coe_mk', CongruenceSubgroup.Gamma_mem', autAdjoinRootXPowSubCEquiv_root, Subgroup.MapSubtype.orderIso_apply_coe, Equiv.Perm.Basis.toCentralizer_equivariant, MonoidHom.restrictHomKerEquiv_apply_coe, Subgroup.isOpen_of_isClosed_of_finiteIndex, MulArchimedeanClass.subgroup_strictAntiOn, ZMod.rootsOfUnity_eq_top, IsSolvable.commutator_lt_of_ne_bot, NumberField.IsCMField.unitsComplexConj_torsion, SubMulAction.ofStabilizer_carrier, Rep.coindResAdjunction_counit_app, Monoid.Coprod.range_inl_sup_range_inr, finEquivZPowers_symm_apply, Subgroup.relIndex_eq_two_iff_exists_notMem_and', MeasureTheory.Subgroup.smulInvariantMeasure, SubMulAction.ofFixingSubgroup_equivariantMap_injective, Subgroup.transferTransversal_apply, GroupExtension.Section.mul_inv_mem_range_inl, Sylow.pointwise_smul_def, Subgroup.pointwise_smul_subset_iff, QuotientGroup.instSecondCountableTopology, DiscreteTiling.PlacedTile.ext_iff_of_preimage, NumberField.InfinitePlace.nat_card_stabilizer_eq_one_or_two, QuotientGroup.borelSpace, IsOfFinOrder.finite_zpowers, MulAut.conjNormal_symm_apply, Subgroup.instCountableSubtypeMulOppositeMemOp, alternatingGroup.isPreprimitive_of_three_le_card, NumberField.InfinitePlace.isUnramified_iff_card_stabilizer_eq_one, Subgroup.index_dvd_two_iff', AddSubgroup.subgroupOf_inertia, QuotientGroup.finite, QuotientGroup.norm_mk_eq_zero, Subgroup.equivOp_symm_apply_coe, fixedPoints_subgroup_iSup, Matrix.SpecialLinearGroup.toGLPos_injective, ProfiniteGrp.limit_one_val, Subgroup.mem_pointwise_smul_iff_inv_smul_mem₀, QuotientGroup.leftRel_r_eq_leftCosetEquivalence, SubMulAction.ofStabilizer.conjMap_comp_inv_apply, Subgroup.subset_pointwise_smul_iff, val_inv_unitarySubgroupUnitsEquiv_symm_apply_coe, Subgroup.le_normalClosure, IsUniformGroup.uniformContinuous_iff_isOpen_ker, nilpotencyClass_quotient_center, Subgroup.map_sup, Subgroup.subgroupOf_inj, QuotientGroup.nhds_eq, AddSubgroup.mem_toSubgroup', Subgroup.op_le_op_iff, isCyclic_iff_exists_zpowers_eq_top, Subgroup.normalCore_eq_iSup, Rep.indToCoindAux_self, Matrix.GeneralLinearGroup.mem_center_iff_val_mem_range_scalar, Finset.doubling_lt_three_halves, MulAut.conjNormal_val, Subgroup.op_iSup, CongruenceSubgroup.exists_Gamma_le_conj', NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst, Subgroup.isClosed_topologicalClosure, DoubleCoset.mem_doubleCoset_self, Equiv.Perm.disjoint_of_disjoint_support, normalClosure_of_stabilizer_eq_top, Rep.indCoindNatIso_hom_app, Subgroup.card_top, ofUnits_le_iff_le_units, Subgroup.instSubgroupClass, Equiv.Perm.Basis.toCentralizer_apply, QuotientGroup.preimage_image_mk, MulAction.stabilizerEquivStabilizer_symm_apply, Set.unit_eq, Group.isNilpotent_iff, SlashInvariantForm.quotientFunc_mk, CongruenceSubgroup.conjGL_coe, CongruenceSubgroup.mem_Gamma_one, Subgroup.map_eq_map_iff, Subgroup.isCoatom_map, Subgroup.map_le_range, cyclotomicCharacter.toZModPow, Sylow.exists_subgroup_card_pow_prime_of_le_card, GroupExtension.Section.mul_inv_mul_mul_mem_range_inl, Subgroup.conjugatesOfSet_subset_normalClosure, AddSubgroup.mem_inertia, Submonoid.inv_mem_units_iff, Subgroup.commutator_def', IsZGroup.coprime_commutator_index, QuotientGroup.rangeKerLift_injective, InfiniteGalois.normalAutEquivQuotient_apply, IsGaloisGroup.fixingSubgroup_top, Subgroup.mem_square, subgroup_solvable_of_solvable, Subgroup.Normal.mem_comm_iff, Equiv.Perm.disjoint_ofSubtype_noncommPiCoprod, Subgroup.subgroupOf_isMulCommutative, DoubleCoset.doubleCoset_union_leftCoset, Valuation.IsRankOneDiscrete.generator_mem_valueGroup, lowerCentralSeries_antitone, Subgroup.map_injective, RootPairing.span_orbit_eq_top, Equiv.Perm.closure_isSwap, groupHomology.comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top, IsGaloisGroup.fixedPoints_top, Equiv.Perm.exists_mem_stabilizer_smul_eq, Equiv.Perm.OnCycleFactors.mem_range_toPermHom_iff', MulAction.stabilizer_mul_self, Set.unitEquivUnitsInteger_symm_apply_coe, alternatingGroup.card_two_sylow_of_card_eq_four, upperCentralSeries_mono, SubMulAction.ofFixingSubgroup_of_inclusion_injective, val_unitarySubgroupUnitsEquiv_symm_apply_coe, frattini_le_comap_frattini_of_surjective, MulEquiv.comapSubgroup_symm_apply, Rep.instIsLeftAdjointSubtypeMemSubgroupCoindFunctorSubtype, QuotientGroup.completeSpace_left, SpecialLinearGroup.mem_center_iff, fixingSubgroup_empty, MulAction.mem_aestabilizer, QuotientGroup.card_quotient_rightRel, RootPairing.range_weylGroup_coweightHom, Subgroup.op_bot, Subgroup.center.smulCommClass_right, MulAction.quotient_out_smul_fixedPoints, DomMulAct.mem_stabilizer_iff, IsGalois.card_fixingSubgroup_eq_finrank, IsPrimitiveRoot.val_toRootsOfUnity_coe, Complex.isQuotientCoveringMap_npow, Subgroup.mem_ofUnits_iff_exists_isUnit, MulAction.IsQuasiPreprimitive.isPretransitive_of_normal, alternatingGroup.kleinFour_card_of_card_eq_four, groupHomology.H1CoresCoinf_X₃, Subgroup.pi_le_iff, derivedSeries_le_map_derivedSeries, GrpCat.SurjectiveOfEpiAuxs.τ_symm_apply_infinity, Subgroup.op_iInf, Subgroup.subgroupOf_eq_top, rootsOfUnity.integer_power_of_ringEquiv, Subgroup.map_one_eq_bot, mem_principal_ideals_iff, Submonoid.units_bot, Group.fg_def, subgroup_units_cyclic, FiniteGaloisIntermediateField.mem_fixingSubgroup_iff, FreeGroup.closure_range_of, Subgroup.pi_bot, MonoidHom.coe_toMultiplicative_range, derivedSeries_zero, Subgroup.le_centralizer_iff, Subgroup.mem_centralizer_iff, Subgroup.apply_coe_mem_map, Subgroup.ofUnits_strictMono, SubMulAction.nat_card_ofStabilizer_add_one_eq, Subgroup.unop_eq_bot, rootsOfUnity.isCyclic, NumberField.InfinitePlace.IsUnramified.stabilizer_eq_bot, IsCyclic.exists_generator, ModularForm.norm_eq_zero_iff, mem_unitarySubgroup_iff, Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_symm_apply_coe_coe, Subgroup.IsSubnormal.iff_eq_top_or_exists, CommGroup.center_eq_top, Equiv.Perm.OnCycleFactors.kerParam_range_card, MulAction.stabilizerEquivStabilizer_trans, GrpCat.SurjectiveOfEpiAuxs.τ_apply_infinity, Subgroup.mul_normal, autAdjoinRootXPowSubCEquiv_symm_smul, MonoidHom.ofLeftInverse_symm_apply, Subgroup.instCountableSubtypeMemZpowers, Monoid.PushoutI.NormalWord.Transversal.compl, Equiv.Perm.exists_mem_stabilizer_isThreeCycle_of_two_lt_ncard, Subgroup.map_inf_eq, QuotientGroup.kerLift_mk', Equiv.Perm.OnCycleFactors.kerParam_injective, MulAction.right_quotientAction, IsCyclic.monoidHom_mulEquiv_rootsOfUnity, Subgroup.isComplement_range_right, SubMulAction.ofStabilizer.inv_conjMap_comp_apply, NumberField.InfinitePlace.card_stabilizer, Subgroup.toSubmonoid_mono, Subgroup.coe_pi, Bot.isCyclic, ModularGroup.coe_apply_complex, IsArithFrobAt.mul_inv_mem_inertia, MulAction.orbit_subgroup_subset, HNNExtension.equiv_eq_conj, QuotientGroup.instDiscreteMeasurableSpace, Subgroup.instIsMulTorsionFree, Subgroup.subgroupOf_self, Subgroup.one_lt_card_iff_ne_bot, OpenSubgroup.toSubgroup_le, Function.MulExact.monoidHom_rangeRestrict, descending_central_series_ge_lower, Subgroup.IsArithmetic.inter, Matrix.SpecialLinearGroup.center_eq_bot_of_subsingleton, Subgroup.smulCommClass_right, MonoidHom.fiberEquivKer_symm_apply, Subgroup.map_comap_eq, rightCoset_eq_iff, MulAction.le_stabilizer_iff_smul_le, OpenSubgroup.toSubgroup_top, Subgroup.commutator_le_right, Subgroup.FG.biSup, Subgroup.comap_injective, MonoidHom.ker_rangeRestrict, Subgroup.le_normalizer_comap, Subgroup.card_eq_one, AlternatingGroup.isPreprimitive_of_three_le_card, Subgroup.IsComplement'.index_eq_card, InfiniteGalois.krullTopology_mem_nhds_one_iff_of_isGalois, mem_rootsOfUnity_prime_pow_mul_iff', finite_zpowers, Subgroup.finiteIndex_iInf, val_unitsCentralizerEquiv_apply_coe, Subgroup.commutator_prod_prod, MulAction.stabilizer_inf_stabilizer_le_stabilizer_sdiff, Equiv.Perm.IsCycle.commute_iff', Subgroup.instHasDetOneMinGeneralLinearGroup_1, Subgroup.map_iSup, SpecialLinearGroup.centerCongr_toLin_equiv_trans_centerEquivRootsOfUnity_eq, Complex.mem_rootsOfUnity, Equiv.altCongrHom_apply_coe, Representation.Coinvariants.le_comap_ker, Equiv.Perm.disjoint_closure_of_disjoint_support, CuspForm.coe_trace, Ideal.rootsOfUnityMapQuot_injective, Subgroup.instDiscreteTopologyQuotientOfContinuousMul, Subgroup.instCovariantClassHSMulLe, NumberField.ComplexEmbedding.IsConj.coe_stabilizer_mk, groupHomology.H1CoresCoinfOfTrivial_X₁, Subgroup.mem_op, mem_rootsOfUnity_iff_mem_nthRoots, Equiv.Perm.alternatingGroup_le_of_index_le_two, QuotientGroup.norm_mk_eq_zero_iff_mem_closure, SubMulAction.map_ofFixingSubgroupUnion_def, CongruenceSubgroup.exists_Gamma_le_conj, DiscreteTiling.PlacedTile.ext_iff_of_exists, Subgroup.exists_ne_one_of_nontrivial, Subgroup.exists_zpowers, finite_iff_subgroup_quotient, Subgroup.Normal.quotient_commutative_iff_commutator_le, Subgroup.pow_mem_of_index_ne_zero_of_dvd, rootsOfUnity.coe_injective, Subgroup.card_bot, Subgroup.bot_or_nontrivial, MonoidHom.ker_eq_top_iff, MulEquiv.mapSubgroup_apply, spinGroup.units_mem_lipschitzGroup, SubMulAction.ofStabilizer.isMultiplyPretransitive_iff, MulAction.Quotient.smul_mk, Ideal.Quotient.stabilizerHom_surjective, disjoint_rootsOfUnity_of_coprime, MonoidHom.transfer_eq_pow_aux, QuotientGroup.con_le_iff, Equiv.Perm.OnCycleFactors.nat_card_range_toPermHom, Subgroup.rank_closure_finite_le_nat_card, alternatingGroup.normalClosure_swap_mul_swap_five, Subgroup.coe_map, MulAction.op_smul_set_stabilizer_subset, Subgroup.mem_adjoinNegOne_iff, Subgroup.quotientCentralizerEmbedding_apply, NumberField.mixedEmbedding.fundamentalCone.integerSetQuotEquivAssociates_apply, Sylow.smul_eq_iff_mem_normalizer, MulAction.mul_stabilizer_self, Subgroup.pointwise_smul_le_pointwise_smul_iff₀, IsTorsion.subgroup, Representation.instIsTrivialSubtypeMemSubgroupSubmoduleInvariantsCompLinearMapIdSubtypeToInvariants, MulArchimedeanClass.mem_subgroup_iff, Subgroup.pi_top, Finset.pow_right_strictMonoOn, MulAction.isBlock_top, Rep.indCoindIso_inv_hom_hom, HNNExtension.inv_t_mul_of, HNNExtension.toSubgroupEquiv_neg_one, alternatingGroup.subsingleton_two_sylow, Subgroup.val_list_prod, MulArchimedeanClass.subsemigroup_eq_subgroup_of_ne_top, QuotientGroup.liftEquiv_coe, IsPGroup.to_quotient, Subgroup.op_top, Monoid.Coprod.closure_range_inl_union_inr, Equiv.Perm.mul_mem_alternatingGroup_of_isSwap, CongruenceSubgroup.Gamma1_mem', MeasureTheory.QuotientMeasureEqMeasurePreimage.mulInvariantMeasure_quotient, Rep.instPreservesProjectiveObjectsActionModuleCatSubtypeMemSubgroupResSubtype, Subgroup.map_inf_le, Subgroup.mem_mk, QuotientGroup.preimage_image_mk_eq_mul, MulAction.ofFixingSubgroup.isMultiplyPreprimitive, Group.IsNilpotent.nilpotent', alternatingGroup.isCoatom_stabilizer_singleton, DoubleCoset.left_bot_eq_left_quot, Subgroup.Normal.conj_smul_eq_self, pow_finEquivZPowers_symm_apply, SlashInvariantForm.coe_translate, QuotientGroup.leftRel_eq, GrpCat.mono_iff_ker_eq_bot, MulAction.IsBlock.stabilizer_le, Equiv.Perm.commute_iff_of_mem_cycleFactorsFinset, Subgroup.coe_equivMapOfInjective_apply, Subgroup.Normal.conjAct, QuotientGroup.completeSpace_right, IntermediateField.fixingSubgroup_top, SubMulAction.ofStabilizer.isPretransitive_iff, Subgroup.mem_ofUnits_iff, QuotientGroup.quotientKerEquivOfRightInverse_apply, MonoidHom.noncommCoprod_range, Subgroup.ofUnits_le_ofUnits_iff, Subgroup.normal_bot, Subgroup.map_le_map_iff_of_injective, least_ascending_central_series_length_eq_nilpotencyClass, MonoidHom.closure_preimage_le, Subgroup.smul_leftQuotientEquiv, MulAction.le_stabilizer_smul_left, rootsOfUnity_one, IsSolvable.commutator_lt_top_of_nontrivial, HasEnoughRootsOfUnity.natCard_rootsOfUnity, upperCentralSeries.map, Subgroup.top_prod, Subgroup.Commensurable.commensurable_conj, Subgroup.pointwise_smul_def, Equiv.Perm.sumCongrHom.card_range, Subgroup.conjAct_pointwise_smul_iff, MulAction.stabilizerEquivStabilizer_compTriple, NumberField.mixedEmbedding.fundamentalCone.integerSetEquiv_apply_fst, Subgroup.isUniformGroup, Subgroup.IsComplement'.isCompl, MeasureTheory.QuotientMeasureEqMeasurePreimage.haarMeasure_quotient, Subgroup.index_ker, Subgroup.normalCore_isClosed, derivedSeries_succ, rootsOfUnity.val_mkOfPowEq_coe, derivedSeries_antitone, Monoid.minOrder_le_natCard, upperCentralSeries_zero, DoubleCoset.right_bot_eq_right_quot, Subgroup.centerCongr_apply_coe, Subgroup.map_top_of_surjective, MulAction.orbitRel.Quotient.mem_subgroup_orbit_iff, Subgroup.mem_map_equiv, RootPairing.weylGroup_apply_root, Subgroup.nontrivial_iff, Subgroup.IsSubnormal.exists_normal_and_le_and_lt_top_of_ne, MulAction.card_eq_sum_card_group_div_card_stabilizer, unitarySubgroupUnitsEquiv_apply_coe, alternatingGroup.characteristic_kleinFour, Subgroup.mem_iSup_prop, Subgroup.nontrivial_iff_exists_ne_one, Subgroup.map_equiv_top, NumberField.Units.span_basisOfIsMaxRank, MonoidHom.range_eq_map, Subgroup.eq_bot_iff_card, Subgroup.finite_quotient_of_finiteIndex, MulEquiv.restrictRootsOfUnity_symm, CommRing.relPic_eq_top, MulAction.IsBlock.orbit_of_normal, IsPrimitiveRoot.coe_autToPow_apply, NumberField.Units.logEmbeddingQuot_apply, Subgroup.coe_inv, Subgroup.finite_iff_finite_and_finiteIndex, DiscreteTiling.PlacedTile.smul_mk_mk, Subgroup.closure_le, mem_closure_isSwap, Subgroup.mem_iInf, Subgroup.div_mem_comm_iff, IsGalois.intermediateFieldEquivSubgroup_apply, MonoidHom.range_one, Subgroup.rank_congr, Subgroup.comap_injective_isMulCommutative, Set.powersetCard.isPretransitive_alternatingGroup, Equiv.Perm.closure_isCycle, QuotientGroup.completeSpace_right', ProfiniteGrp.denseRange_toLimit, DiscreteTiling.PlacedTile.ext_iff, alternatingGroup.kleinFour_isKleinFour, Subgroup.exists_mem_ofUnits_val_eq, Subgroup.instFiniteIndexMin, ProfiniteGrp.closedSubgroup_eq_sInf_open, AlternatingGroup.card_of_cycleType_singleton, Rep.indCoindIso_hom_hom_hom, Subgroup.leftCoset_cover_const_iff_surjOn, SubMulAction.fixingSubgroup_of_insert, Subgroup.coe_square, Subgroup.FG.finset_sup, QuotientGroup.liftEquiv_mk, CommGroup.coe_primaryComponent, MulEquiv.subgroupCongr_apply, Subgroup.closure_closure_coe_preimage, Con.mem_subgroup_iff, Subgroup.subtype_apply, SubMulAction.ofFixingSubgroup_carrier, alternatingGroup.normalClosure_finRotate_five, Subgroup.normalClosure_subset_iff, groupHomology.H1CoresCoinf_X₁, Subgroup.subset_normalizer_of_normal, Subgroup.smul_diff_smul', Subgroup.mem_of_mem_val_ofUnits, Subgroup.coe_subtype, QuotientGroup.eq_class_eq_leftCoset, ClosedSubgroup.toSubgroup_injective, Subgroup.centerToMulOpposite_apply_coe, Subgroup.rank_le_index_mul_rank, groupCohomology.infNatTrans_app, CongruenceSubgroup.Gamma_one_top, NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul_smul_coe, Set.coe_unit, Ideal.card_stabilizer_eq, Subgroup.mem_goursatFst, Subgroup.subtype_injective, Subgroup.top_toSubmonoid, Subgroup.isComplement'_bot_right, QuotientGroup.nontrivial_iff, Subgroup.index_mul_card, top_fixedByFinite, alternatingGroup.kleinFour_eq_commutator, QuotientGroup.nhds_one_hasBasis, Subgroup.fg_iff_add_fg, Rep.indToCoindAux_fst_mul_inv, Subgroup.set_mul_normal_comm, Subgroup.le_topologicalClosure, Subgroup.Commensurable.commensurator_mem_iff, infinite_zpowers, map_derivedSeries_le_derivedSeries, IsDedekindDomain.selmerGroup.monotone, Valuation.mem_unitGroup_iff, GroupExtension.Section.inv_mul_mem_range_inl, QuotientGroup.congr_symm, DiscreteTiling.Prototile.ext_iff, HasEnoughRootsOfUnity.rootsOfUnity_isCyclic, Set.subgroupClosure_mul_pow, Subgroup.mem_pi, MulAction.isPreprimitive_ofFixingSubgroup_conj_iff, Subgroup.le_centralizer, Subgroup.toSubmonoid_strictMono, Subgroup.instIsTopologicalGroupSubtypeMem, Subgroup.instFiniteIndex_subgroupOf, Subgroup.isComplement_subgroup_left_iff_existsUnique_quotientMk'', Subgroup.op_inf, Subgroup.card_commutator_le_of_finite_commutatorSet, QuotientGroup.instIsMulTorsionFree, Subgroup.zpowers_le, IsPGroup.to_subgroup, Subgroup.pi_empty, Equiv.Perm.Basis.card_ofPermHom_support, Subgroup.mem_center_iff, MonoidHom.range_eq_bot_iff, QuotientGroup.rightRel_r_eq_rightCosetEquivalence, IsPrimitiveRoot.card_rootsOfUnity', alternatingGroup.center_eq_bot, alternatingGroup.stabilizer.surjective_toPerm, Subgroup.coe_ofClass, IsGaloisGroup.fixedPoints_fixingSubgroup, SubMulAction.mem_fixingSubgroup_insert_iff, Subgroup.centralizer_eq_top_iff_subset, Subgroup.negOne_mem_adjoinNegOne, isCancelSMul_iff_stabilizer_eq_bot, Subgroup.smul_opposite_image_mul_preimage, Units.val_set_image_rootsOfUnity_one, Subgroup.characteristic_iff_comap_le, Equiv.Perm.Basis.ofPermHom_apply, FiniteField.sum_subgroup_units_eq_zero, ModularGroup.SL_to_GL_tower, Subgroup.coe_pow, Representation.ofQuotient_coe_apply, QuotientGroup.univ_eq_iUnion_smul, Subgroup.normal_subgroupOf_iff_le_normalizer_inf, SubMulAction.ofStabilizer.isMultiplyPretransitive_iff_of_conj, Subgroup.characteristic_iff_map_le, MulArchimedeanClass.mem_closedBallSubgroup_iff, FiniteMulArchimedeanClass.mem_ballSubgroup_iff, ValuationSubring.principalUnitGroup_le_principalUnitGroup, Subgroup.comap_lt_comap_of_surjective, leftCoset_eq_iff, IsGaloisGroup.le_fixedPoints_iff_le_fixingSubgroup, Rep.indToCoindAux_comm, Subgroup.normal_top, MonoidHom.restrictHomKerEquiv_symm_coe_apply, GrpCat.ker_eq_bot_of_mono, IsGaloisGroup.fixingSubgroup_le_of_le, Circle.isQuotientCoveringMap_zpow, MonoidWithZeroHom.valueGroup_eq_range, Subgroup.commutator_le, Subgroup.noncommPiCoprod_apply, Subgroup.normalizerMonoidHom_ker, LinearIsometryEquiv.reflections_generate, Subgroup.FG.biSup_finset, least_descending_central_series_length_eq_nilpotencyClass, MonoidHom.restrict_range, FiniteMulArchimedeanClass.mem_closedBallSubgroup_iff, IntermediateField.fixedField_antitone, Subgroup.comap_sup_eq, Valuation.IsRankOneDiscrete.instIsCyclicSubtypeUnitsMemSubgroupValueGroup, MulAction.isCoatom_stabilizer_iff_preprimitive, CommGroup.isMulTorsionFree_iff_torsion_eq_bot, MulAction.card_eq_sum_card_group_div_card_stabilizer', MonoidHom.range_isMulCommutative, Subgroup.ker_subtype, AddSubgroup.toSubgroup_closure, Equiv.Perm.OnCycleFactors.mem_range_toPermHom'_iff, Sylow.not_dvd_card_commutator_or_not_dvd_index_commutator, Subgroup.sylow_mem_fixedPoints_iff, card_commutatorSet_closureCommutatorRepresentatives, InfiniteGalois.mulEquivToLimit_symm_continuous, modularCyclotomicCharacter.toFun_spec, CongruenceSubgroup.IsArithmetic.conj, isQuotientCoveringMap_npow, Subgroup.coe_norm, Subgroup.centralizer_closure, MulChar.apply_mem_rootsOfUnity_of_pow_eq_one, NumberField.Units.fundSystem_mk, Rep.coindResAdjunction_unit_app, MulAction.IsBlock.orbit_stabilizer_eq, upperCentralSeries_nilpotencyClass, Equiv.Perm.swap_mem_stabilizer, Monoid.CoprodI.range_eq_iSup, QuotientGroup.eq, CongruenceSubgroup.Gamma_cong_eq_self, Subgroup.le_pi_iff, MulEquiv.restrictRootsOfUnity_coe_apply, Subgroup.discrete_iff_cyclic, IsOfFinOrder.mem_zpowers_iff_mem_range_orderOf, NumberField.IsCMField.indexRealUnits_mul_eq, Subgroup.mem_zpowers, NumberField.Units.dirichletUnitTheorem.map_logEmbedding_sup_torsion, QuotientGroup.instT2Space, groupHomology.H1CoresCoinf_g, IsPrimitiveRoot.card_rootsOfUnity, MulAction.stabilizerEquivStabilizer_apply, InfiniteGalois.isOpen_mulEquivToLimit_image_fixingSubgroup, CoxeterSystem.subgroup_closure_range_simple, QuotientGroup.subgroup_eq_top_of_subsingleton, stabilizer_empty_eq_top, IsSimpleGroup.instIsSimpleOrderSubgroup, HasEnoughRootsOfUnity.cyc, MulEquiv.coe_comapSubgroup, Subgroup.normalizer_eq_top, Subgroup.closure_empty, Subgroup.instCanLiftSetCoeAndMemOfNatForallForallForallForallHMulForallForallInv, Subgroup.mem_toAddSubgroup', Subgroup.index_inf_le, MonoidHom.subtype_comp_rangeRestrict, Subgroup.prod_eq_bot_iff, Subgroup.pointwise_isCentralScalar, Ideal.Quotient.stabilizerHom_surjective_of_profinite, NumberField.mixedEmbedding.fundamentalCone.unit_smul_mem_iff_mem_torsion, isClosed_nullSubgroup, MulAction.stabilizer_finset_univ, ValuationSubring.coe_unitGroupMulEquiv_apply, Subgroup.coe_top, Sylow.conj_eq_normalizer_conj_of_mem, NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul_stabilizer, ofAdd_image_zmultiples_eq_zpowers_ofAdd, Subgroup.smul_apply_eq_smul_apply_inv_smul, NumberField.Units.rank_modTorsion, Subgroup.IsComplement'.card_mul, Equiv.Perm.closure_cycle_coprime_swap, Subgroup.isCyclic_zpowers, Ideal.inertia_le_stabilizer, map_commutator_eq, ValuationSubring.unitGroup_injective, Subgroup.inf_subgroupOf_inf_normal_of_left, Subgroup.relIndex_map_map, SubMulAction.disjoint_val_image, Units.val_set_image_rootsOfUnity, Action.FintypeCat.toEndHom_apply, QuotientGroup.mk'_apply, IsGalois.normalAutEquivQuotient_apply, QuotientGroup.rangeKerLift_surjective, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_pow', Subgroup.mem_map_iff_mem, Rep.coindToInd_apply, Subgroup.mem_inv_pointwise_smul_iff₀, Group.rank_spec, Subgroup.subgroupOf_eq_bot, alternatingGroup.coe_kleinFour_of_card_eq_four, MulAction.IsPreprimitive.isCoatom_stabilizer_of_isPreprimitive, Equiv.Perm.subtypeCongrHom.card_range, Subgroup.normal_inf_normal, Subgroup.normalCore_eq_iInf_conjAct, Monoid.Coprod.range_swap, MonoidHom.coe_toAdditive_map, Subgroup.card_range_dvd, MulAction.mem_stabilizer_finset, ValuationSubring.mem_unitGroup_iff, CongruenceSubgroup.isArithmetic_conj_SL2Z, Subgroup.relIndex_eq_two_iff_exists_notMem_and, Subgroup.index_eq_zero_iff_infinite, HNNExtension.NormalWord.unitsSMulGroup_snd, subgroupIsFreeOfIsFree, QuotientGroup.quotientKerEquivOfRightInverse_symm_apply, nilpotent_iff_lowerCentralSeries, Rep.resIndAdjunction_homEquiv_symm_apply, Subgroup.relIndex_eq_two_iff, Subgroup.mem_closure_range_iff_of_fintype, Subgroup.pi_eq_bot_iff, GrpCat.SurjectiveOfEpiAuxs.agree, HNNExtension.NormalWord.unitsSMul_one_group_smul, Subgroup.normal_iInf_normal, Subgroup.fg_of_index_ne_zero, Group.fg_iff, powers_eq_zpowers, Subgroup.index_iInf_le, Subgroup.map_lt_map_iff_of_injective, SubMulAction.nat_card_ofStabilizer_eq, MonoidHom.fiberEquivKer_apply, Subgroup.isComplement'_top_right, PresentedGroup.closure_rels_subset_ker, Subgroup.normal_le_normalCore, Finset.invMulSubgroup_eq_mul_inv, Subgroup.commGroup_isMulCommutative, Subgroup.rank_commutator_le_card, OpenSubgroup.toSubgroup_inf, MulAction.coe_quotient_smul_fixedPoints, GroupExtension.Section.mul_mul_mul_inv_mem_range_inl, QuotientGroup.eq_iff_div_mem, MulAction.stabilizer_subgroup, NumberField.IsCMField.unitsMulComplexConjInv_apply_torsion, Subgroup.map_subtype_le_map_subtype, Subgroup.mk_le_mk, Subgroup.coe_toAddSubgroup_symm_apply, Equiv.Perm.Basis.ofPermHom_mem_centralizer, MulAction.finite_quotient_of_finite_quotient_of_finite_quotient, Subgroup.mem_sup_of_normal_right, Subgroup.coe_zpow, IsGaloisGroup.fixingSubgroup_fixedPoints, IsFractionRing.stabilizerHom_surjective, Subgroup.prod_mono, Submonoid.units_isCompact, Subgroup.instFiniteIndexTop, Subgroup.mem_closure_singleton, MulAction.stabilizer_finset_empty, Subgroup.pow_index_mem, Subgroup.coe_pathComponentOne, groupCohomology.H1InfRes_X₃, Subgroup.index_eq_two_iff, SpecialLinearGroup.centerEquivRootsOfUnity_symm_apply, Subgroup.relIndex_sup_right, IsZGroup.instSubtypeMemSubgroup, MulAction.mem_stabilizer_set_iff_subset_smul_set, Units.mem_posSubgroup, Submonoid.units_top, Subgroup.bot_or_exists_ne_one, Subgroup.closure_singleton_one, Unitization.val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, DiscreteTiling.PlacedTile.coe_mk_mk, ProfiniteGrp.limit_mul_val, MonoidHom.mem_ker, Ideal.Quotient.stabilizerHom_apply, Subgroup.center_le_normalizer, ofMul_image_zpowers_eq_zmultiples_ofMul, NumberField.mixedEmbedding.fundamentalCone.quotIntNorm_apply, QuotientGroup.dense_preimage_mk, Rep.indToCoindAux_mul_fst, MulEquiv.coe_mapSubgroup, Subgroup.mem_closure_range_iff, Finset.doubling_lt_two, Subgroup.commutator_comm, NumberField.Units.mem_torsion, Submonoid.isOpen_units, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, map_rootsOfUnity_eq_pow_self, MulAction.smul_set_stabilizer_subset, Subgroup.card_map_dvd, Equiv.Perm.support_zpowers_of_mem_cycleFactorsFinset_le, Submonoid.units_sInf, QuotientGroup.mk'_comp_subtype, Sylow.normalizer_le_centralizer_or_le_commutator, IsCyclic.card_powMonoidHom_ker, mem_lowerCentralSeries_succ_iff, Subgroup.mem_smul_pointwise_iff_exists, instIsModularLatticeSubgroup, Equiv.Perm.stabilizer_isPreprimitive, Subgroup.val_centerUnitsEquivUnitsCenter_symm_apply_coe, Subgroup.ext_iff, NumberField.Units.regOfFamily_div_regulator, QuotientGroup.mk'_eq_mk', IsPGroup.ker_isPGroup_of_injective, IsGaloisGroup.fixedPoints_bot, Subgroup.zpowers_isMulCommutative, Subgroup.commutator_pi_pi_le, Subgroup.relIndex_bot_left, Subgroup.le_normalizer, Subgroup.disjoint_def', Equiv.Perm.mem_alternatingGroup, Subgroup.instFiniteSubtypeMemCommutatorOfElemCommutatorSet, Subgroup.relIindex_dvd_two_iff', MulAction.isPretransitive_quotient, Subgroup.orderIsoCon_apply, normal_iff_eq_cosets, Subgroup.index_dvd_two_iff, IntermediateField.fixingSubgroup_le, Subgroup.map_eq_bot_iff, MulAction.stabilizer_subset_div_right, PresentedGroup.mk_eq_one_iff, Subgroup.isClosed_of_discrete, Subgroup.inf_relIndex_right, Finset.doubling_lt_golden_ratio, Valuation.IsRankOneDiscrete.generator_zpowers_eq_range, Matrix.SpecialLinearGroup.scalar_eq_coe_self_center, IsGaloisGroup.ofDual_intermediateFieldEquivSubgroup_apply, MulAction.isPreprimitive_fixingSubgroup_insert_iff, QuotientGroup.measurableSMul, Subgroup.inf_subgroupOf_right, Subgroup.characteristic_iff_le_comap, HNNExtension.of_mul_t, Rep.resIndAdjunction_homEquiv_apply, MulAction.mem_stabilizer_set', Subgroup.iSup_comap_le, Equiv.Perm.OnCycleFactors.val_centralizer_smul, Subgroup.one_mem, Subgroup.topEquiv_symm_apply_coe, Subgroup.normalizerMonoidHom_apply_apply_coe, Subgroup.card_commutator_dvd_index_center_pow, IsQuotientCoveringMap.subgroup_congr, IsPGroup.cyclic_center_quotient_of_card_eq_prime_sq, Sylow.le_center_or_le_commutator, IsGalois.intermediateFieldEquivSubgroup_symm_apply_toDual, Subgroup.exists_isComplement_left, Subgroup.closure_mono, FiniteIndexNormalSubgroup.toSubgroup_injective, Subgroup.topologicalClosure_coe, Subgroup.rank_closure_finset_le_card, CuspForm.coe_translate, ProperlyDiscontinuousSMul.finite_stabilizer, HNNExtension.of_mul_inv_t, AddChar.val_mem_rootsOfUnity, NumberField.IsCMField.closure_realFundSystem_sup_torsion, Subgroup.comap_inf, bijective_rootsOfUnityAddChar, NumberField.Units.instIsCyclicSubtypeUnitsRingOfIntegersMemSubgroupTorsion, DoubleCoset.rel_bot_eq_right_group_rel, SpecialLinearGroup.SL2Z_generators, MeasureTheory.QuotientMeasureEqMeasurePreimage.smulInvariantMeasure_quotient, Submonoid.units_surjective, Rep.quotientToInvariantsFunctor_map_hom, MulAction.stabilizer_univ, Set.val_unitEquivUnitsInteger_apply_coe, SubMulAction.ofFixingSubgroup_of_eq_apply, Ideal.Quotient.stabilizerQuotientInertiaEquiv_mk, MulAction.stabilizer_subgroup_op, Subgroup.FG.sup, MonoidHom.div_mem_ker_iff, Subgroup.commutator_le_self, MonoidHom.transfer_center_eq_pow, Rep.quotientToCoinvariantsFunctor_map_hom, DihedralGroup.center_eq_bot_of_odd_ne_one, MulArchimedeanClass.ballSubgroup_antitone, Subgroup.commutator_eq_bot_iff_le_centralizer, Submonoid.units_left_inverse, Subgroup.instMeasurableConstSMul, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_apply, Subgroup.map_bot, Sylow.commutator_eq_bot_or_commutator_eq_self, Subgroup.noncommPiCoprod_mulSingle, swap_mem_closure_isSwap, Subgroup.disjoint_def, Subgroup.map_centralizer_le_centralizer_image, SubMulAction.nat_card_ofStabilizer_eq_add_one, MulEquiv.mapSubgroup_symm_apply, IntermediateField.fixingSubgroup_antitone, Rep.coindResAdjunction_homEquiv_apply, mem_fixingSubgroup_compl_iff_movedBy_subset, Subgroup.coe_set_mk, MonoidHom.coe_comp_rangeRestrict, MulAction.stabilizer_empty, Subgroup.mem_ofUnits_iff_toUnits_mem, Subgroup.comap_sup_comap_le, rootsOfUnity.coe_mkOfPowEq, IsPGroup.bot_lt_center, ValuationSubring.unitGroup_strictMono, RootPairing.isSimpleModule_weylGroupRootRep, AlternatingGroup.card_of_cycleType, Subgroup.mem_comap, Subgroup.ofUnits_inf, QuotientGroup.discreteTopology_iff, Rep.coinvariantsShortComplex_f, Subgroup.normalClosure_eq_iInf, Subgroup.IsSubnormal.eq_bot_or_top_of_isSimpleGroup, Rep.resIndAdjunction_counit_app, DiscreteTiling.PlacedTile.smul_mk_coe, NumberField.Units.closure_fundSystem_sup_torsion_eq_top, RootPairing.InvariantForm.apply_weylGroup_smul, Equiv.Perm.Basis.toPermHom_apply_toCentralizer, Subgroup.top_prod_top, Subgroup.quotientiInfSubgroupOfEmbedding_apply_mk, Subgroup.unop_sInf, QuotientGroup.kerLift_injective, Subgroup.dense_or_cyclic, SubMulAction.ofFixingSubgroup.isMultiplyPretransitive, instIsInvariantSubtypeMemSubalgebraSubalgebraSubgroupQuotient, Subgroup.index_bot, RootPairing.isSimpleModule_weylGroupRootRep_iff, Subgroup.normalClosure_mono, CommGrpCat.range_eq_top_of_epi, Subgroup.relIndex_inf_mul_relIndex, ofUnits_units_gc, MulAction.finite_quotient_of_pretransitive_of_finite_quotient, Subgroup.coe_iInf, QuotientGroup.mk_out_eq_mul, Subgroup.instHasDetOneMinGeneralLinearGroup, Subgroup.commutator_bot_right, Equiv.Perm.finRotate_bit1_mem_alternatingGroup, SubMulAction.ENat_card_ofStabilizer_add_one_eq, Equiv.Perm.centralizer_le_alternating_iff, QuotientGroup.instT3Space, Subgroup.quotientEquivSigmaZMod_apply, pinGroup.units_mem_iff, Subgroup.finiteIndex_iInf', Subgroup.exponent_toSubmonoid, Subgroup.exponent_top, Subgroup.mem_centralizer_singleton_iff, Subgroup.le_prod_iff, Equiv.Perm.OnCycleFactors.mem_ker_toPermHom_iff, NumberField.Units.torsion_eq_one_or_neg_one_of_odd_finrank, instIsMulCommutativeSubtypeMemSubgroupOfIsCyclic, surjective_rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar, Set.pow_mul_subgroupClosure, surjective_cosetToCuspOrbit, Equiv.Perm.Basis.ofPermHom_support, Subgroup.map_subtype_lt_map_subtype, IntermediateField.fixingSubgroup_isClosed, Subgroup.map_le_map_iff, MulAction.orbitRel.Quotient.subgroup_quotient_eq_iff, coe_smul_fixedPoints_of_normal, RootPairing.reflection_mem_weylGroup, MulAction.stabilizer_op_subgroup, Action.FintypeCat.quotientToEndHom_mk, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_pow, Subgroup.normal_mul, QuotientGroup.congr_apply, CategoryTheory.PreGaloisCategory.nhds_one_has_basis_stabilizers, Module.stabilizer_units_eq_bot_of_ne_zero, HahnSeries.binomial_power, QuotientGroup.orbit_eq_out_smul, MulAction.mem_subgroup_orbit_iff, NumberField.InfinitePlace.isRamified_iff_card_stabilizer_eq_two, Subgroup.comap_map_eq, Subgroup.eq_top_iff', Subgroup.closure_le_centralizer_centralizer, Submonoid.units_inf, Equiv.Perm.mem_sumCongrHom_range_of_perm_mapsTo_inl, Subgroup.subgroupOf_map_subtype, NumberField.Units.dirichletUnitTheorem.logEmbedding_eq_zero_iff, QuotientGroup.preimage_image_mk_eq_iUnion_image, Subgroup.closure_eq_top_of_mclosure_eq_top, ConjAct.normal_of_characteristic_of_normal, Subgroup.mem_sup, MulAction.stabilizer_le_aestabilizer, Sylow.exists_subgroup_card_pow_prime, Multiplicative.mem_toSubgroup, Monoid.Coprod.range_lift, Subgroup.commutator_def, QuotientGroup.mk_pow, Subgroup.exists_mem_zpowers, val_unitsCentralizerEquiv_symm_apply_coe, Subgroup.instFiniteQuotientSubtypeMemOpenSubgroupOfIsTopologicalGroupOfCompactSpace, isNilpotent_of_finite_tfae, Subgroup.card_le_card_group, QuotientGroup.continuous_mk, SubMulAction.notMem_val_image, Submodule.unitsQuotEquivRelPic_symm_apply, lowerCentralSeries_pi_le, CongruenceSubgroup.finiteIndex_conjGL, QuotientGroup.range_mk', Subgroup.map_eq_bot_iff_of_injective, lowerCentralSeries.map, Subgroup.ofUnits_mono, QuotientGroup.range_mk, MulAction.orbitZPowersEquiv_symm_apply, MonoidHom.range_eq_top, Representation.instIsTrivialSubtypeMemSubgroupCoinvariantsCompLinearMapIdSubtypeToCoinvariants, Rep.indToCoindAux_mul_snd, HNNExtension.t_mul_of, Subgroup.Commensurable.commensurable_inv, Subgroup.sq_mem_of_index_two, Subgroup.ofUnits_inf_units, Subgroup.val_centerUnitsEquivUnitsCenter_apply_coe, Subgroup.instIsScalarTowerSubtypeMem, Equiv.Perm.Basis.ofPermHomFun_apply_mem_support_cycle_iff, Monoid.PushoutI.inf_of_range_eq_base_range, Subgroup.ker_le_comap, Subgroup.exists_inv_mem_iff_exists_mem, Subgroup.toAddSubgroup_closure, alternatingGroup.two_sylow_eq_kleinFour_of_card_eq_four, QuotientGroup.strictMono_comap_prod_image, Subgroup.map_le_map_iff', mem_zpowers_pow_iff, MulEquiv.comapSubgroup_apply, Matrix.SpecialLinearGroup.coe_GLPos_neg, QuotientGroup.homQuotientZPowOfHom_comp_of_rightInverse, Circle.isQuotientCoveringMap_npow, MonoidHom.mem_range, alternatingGroup.nontrivial_of_three_le_card, Subgroup.op_eq_top, isQuotientCoveringMap_zpow, MulAction.stabilizer_quotient, MulAction.mem_stabilizer_set, Subgroup.coe_mul, isZGroup_iff_exists_mulEquiv, MulAction.IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup, comap_upperCentralSeries_quotient_center, Subgroup.center.smulCommClass_left, HahnSeries.pow_add, mem_upperCentralSeriesStep, Subgroup.mul_self_mem_of_index_two, NumberField.IsCMField.unitsMulComplexConjInv_ker, Subgroup.op_sInf, Rep.toCoinvariantsMkQ_hom, Subgroup.normal_subgroupOf, Subgroup.isComplement'_bot_left, MulAction.mem_stabilizer_finset_iff_smul_finset_subset, Subgroup.coe_toAddSubgroup_apply, Subgroup.Commensurable.conj, MulAction.isMultiplyPreprimitive_iff, MulAction.Quotient.mk_smul_out, Subgroup.forall_zpowers, Equiv.swap_mem_stabilizer, Equiv.Perm.IsCycle.zpowersEquivSupport_apply, Subgroup.isNilpotent, Subgroup.subsingleton_iff, Subgroup.subset_closure, ValuationSubring.unitGroup_le_unitGroup, CongruenceSubgroup.ModularGroup_T_pow_mem_Gamma, Subgroup.commutator_le_inf, Subgroup.mem_goursatSnd, Subgroup.bot_toSubmonoid, ValuationSubring.principal_units_le_units, QuotientGroup.fg, rootsOfUnity_inf_rootsOfUnity, Equiv.Perm.OnCycleFactors.cycleType_kerParam_apply_apply, MonoidHom.rangeRestrict_surjective, Subgroup.comap_le_comap_of_surjective, Subgroup.index_ne_zero_iff_finite, MonoidHom.coe_graph, IsGalois.intermediateFieldEquivSubgroup_symm_apply, MulAction.map_stabilizer_le, CommGrpCat.mono_iff_ker_eq_bot, Subgroup.transferTransversal_apply', Sylow.card_eq_multiplicity, lowerCentralSeries_eq_bot_iff_nilpotencyClass_le, pinGroup.units_mem_lipschitzGroup, Subgroup.continuousSMul, QuotientGroup.map_normal, Topology.IsQuotientMap.isCoveringMapOn_of_smul_disjoint, RootPairing.range_weylGroupToPerm, Function.MulExact.iff_monoidHom_rangeRestrict, AlternatingGroup.isMultiplyPretransitive, QuotientGroup.instContinuousSMul, Matrix.GeneralLinearGroup.mem_center_iff_val_eq_scalar, Subgroup.smul_closure, MulAction.orbitEquivQuotientStabilizer_symm_apply, Subgroup.relIndex_iInf_le, Subgroup.mem_closure_of_mem, alternatingGroup.exists_mem_stabilizer_smul_eq, SpecialLinearGroup.centerEquivRootsOfUnity_apply, MulAction.aestabilizer_empty, isSolvable_def, FiniteMulArchimedeanClass.mem_subgroup_iff, alternatingGroup.coe_two_sylow_of_card_eq_four, Group.rank_range_le, NumberField.IsCMField.unitsMulComplexConjInv_apply, Subgroup.closure_univ, Set.unit_valuation_eq_one, Subgroup.eq_bot_or_eq_top_of_prime_card, IsZGroup.commutator_lt, commutator_centralizer_commutator_le_center, IsGalois.fixedField_top, MulActionHom.toQuotient_apply, QuotientGroup.homQuotientZPowOfHom_comp, groupCohomology.H1InfRes_X₁, MulAction.orbitRel_subgroupOf, lowerCentralSeries_succ, SubMulAction.mem_ofStabilizer_iff, Subgroup.map_subtype_le, QuotientGroup.subsingleton_quotient_top, Subgroup.index_toAddSubgroup, Rep.quotientToInvariantsFunctor_obj_V, SubMulAction.ofStabilizer.snoc_castSucc, stabilizer_isOpen_of_isIntegral, Subgroup.quotientiInfEmbedding_apply_mk, Subgroup.card_subgroup_dvd_card, QuotientGroup.exists_norm_mk_lt, Subgroup.IsFiniteRelIndex.to_finiteIndex_subgroupOf, Topology.IsQuotientMap.isCoveringMapOn_of_properlyDiscontinuousSMul, FixedPoints.mem_subgroup, Subgroup.mem_sInf, Subgroup.relIindex_eq_two_iff', normalizerCondition_iff_only_full_group_self_normalizing, lowerCentralSeries_map_subtype_le, Subgroup.finiteIndex_iff_finite_quotient, SubMulAction.mem_ofFixingSubgroup_insert_iff, MulAction.coe_aestabilizer, QuotientGroup.completeSpace_left', Subgroup.quotientiInfEmbedding_apply, MulAction.isMultiplyPreprimitive_succ_iff_ofStabilizer, NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates_eq_iff, Subgroup.le_comap_map, SlashInvariantForm.coe_trace, Equiv.Perm.OnCycleFactors.coe_toPermHom, Subgroup.prod_top, SpecialLinearGroup.center_eq_bot_of_finrank_le_one, dense_submonoidClosure_iff_subgroupClosure, Subgroup.isComplement_range_left, Equiv.Perm.exists_mem_stabilizer_isThreeCycle, closure_submonoidClosure_eq_closure_subgroupClosure, MonoidHom.transferCenterPow_apply, Subgroup.mem_closure_singleton_iff_existsUnique_zpow, ClassGroup.equivPic_symm_apply, Equiv.Perm.eq_top_of_isMultiplyPretransitive, NumberField.IsCMField.mem_realUnits_iff, Subgroup.card_quotient_dvd_card, two_mul_card_alternatingGroup, Subgroup.pointwise_smul_le_iff₀, commutator_alternatingGroup_eq_top, Monoid.le_minOrder_iff_forall_subgroup, MonoidHom.ker_eq_bot_of_cancel, MonoidHom.coe_rangeRestrict, Finset.le_card_quotient_mul_sq_inter_subgroup, Subgroup.mem_normalizer_iff, SubMulAction.ofStabilizer.conjMap_comp, groupCohomology.H1InfRes_g, Subgroup.smul_sup, fixingSubgroup_iUnion, Subgroup.instFGSubtypeMemCommutator, QuotientGroup.congr_mk', Equiv.Perm.sigmaCongrRightHom.card_range, RootPairing.weylGroup.ofIdx_smul, QuotientGroup.mk_inv, MulAction.mem_stabilizer_set_iff_smul_set_subset, MonoidHom.coe_toAdditive_range, ConjClasses.mk_bijOn, Subgroup.eq_bot_iff_forall, mem_upperCentralSeries_succ_iff, Representation.le_comap_invariants, Subgroup.map_eq_range_iff, Group.fg_iff_subgroup_fg, Rep.indCoindNatIso_inv_app, MonoidHom.range_eq_top_of_surjective, QuotientGroup.rightRel_apply, MulAction.zpowersQuotientStabilizerEquiv_symm_apply, Subgroup.smul_def, MonoidHom.ker_fst, NumberField.IsCMField.unitsComplexConj_eq_self_iff, Subgroup.prod_le_iff, HNNExtension.toSubgroupEquiv_neg_apply, ValuationSubring.surjective_unitGroupToResidueFieldUnits, Equiv.Perm.swap_mul_swap_same_mem_closure_three_cycles, Subgroup.instMeasurableSMul, AlternatingGroup.isPretransitive_of_three_le_card, Subgroup.coe_one, Subgroup.prod_mono_left, IsGaloisGroup.intermediateField, Subgroup.mem_closure_pair, MulAction.injective_ofQuotientStabilizer, Subgroup.finite_quotient_of_pretransitive_of_index_ne_zero, derived_le_lower_central, DoubleCoset.rel_iff, MonoidHom.noncommPiCoprod_range, Subgroup.coe_unop, Rep.coindResAdjunction_homEquiv_symm_apply, ValuationSubring.principalUnitGroupEquiv_apply, closure_of_isSwap_of_isPretransitive, Subgroup.coe_inf, nilpotent_iff_finite_descending_central_series, Subgroup.bot_subgroupOf, Subgroup.relIndex_inf_le, Subgroup.map_le_iff_le_comap, Subgroup.coe_topologicalClosure_bot, Subgroup.equivOp_apply_coe, CongruenceSubgroup.Gamma1_in_Gamma0, Subgroup.Normal.subgroupOf, card_alternatingGroup, IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply, MulAction.orbitZPowersEquiv_symm_apply', alternatingGroup.stabilizer_isPreprimitive, Nat.card_zpowers, Subgroup.index_eq_two_iff_exists_notMem_and', Submonoid.mem_units_iff, Subgroup.smul_opposite_mul, IsDedekindDomain.selmerGroup.fromUnit_ker, ConjAct.Subgroup.val_conj_smul, Subgroup.opEquiv_symm_apply, Equiv.Perm.prod_list_swap_mem_alternatingGroup_iff_even_length, Subgroup.smul_inf, Subgroup.relIndex_sup_left, MulAction.stabilizer_image_coe_quotient, SubMulAction.ofStabilizer.isMultiplyPretransitive, coe_set_eq_one, CongruenceSubgroup.Gamma1_mem, SubMulAction.ofFixingSubgroup.append_right, mapClusterPt_atTop_pow_iff_mem_topologicalClosure_zpowers, Subgroup.isComplement'_top_bot, Subgroup.relIndex_eq_one, Subgroup.unit_mem_of_mem_ofUnits, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow', IntermediateField.finrank_fixedField_eq_card, Subgroup.toIsOrderedMonoid, MonoidHom.range_eq_top_of_cancel, Subgroup.FG.iSup, QuotientGroup.isOpenMap_coe, Subgroup.discreteTopology_iff_of_finiteIndex, two_mul_nat_card_alternatingGroup, Ideal.card_inertia_eq_ramificationIdxIn, Valuation.instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial, Equiv.Perm.IsSwap.mul_mem_closure_three_cycles, Subgroup.unop_eq_top, MonoidHom.ofLeftInverse_apply, mem_zpowers_zpow_iff, MonoidHom.eq_iff, Equiv.Perm.IsThreeCycle.alternating_normalClosure, Subgroup.zpowers_eq_bot, Matrix.SpecialLinearGroup.eq_scalar_center_equiv_rootsOfUnity, solvable_quotient_of_solvable, Subgroup.coe_center, mem_zpowers_of_prime_card, Subgroup.normalizer_eq_top_iff, CongruenceSubgroup.mem_conjGL, Subgroup.unop_iSup, Subgroup.closure_mul_le, instFiniteElemSubtypeMemSubgroupClosureCommutatorRepresentativesCommutatorSet, NumberField.InfinitePlace.not_isUnramified_iff_card_stabilizer_eq_two, Subgroup.ker_subgroupMap, Subgroup.isComplement_subgroup_left_iff_bijective, Matrix.SpecialLinearGroup.coe_to_GLPos_to_GL_det, Units.val_set_image_rootsOfUnity_two, ValuationSubring.mem_principalUnitGroup_iff, IsSimpleGroup.eq_bot_or_eq_top_of_normal, QuotientGroup.exists_norm_mul_lt, alternatingGroup.normal_kleinFour, Equiv.Perm.subgroup_eq_top_of_nontrivial, Subgroup.isComplement'_iff_card_mul_and_disjoint, card_commutator_closureCommutatorRepresentatives, QuotientGroup.equivQuotientZPowOfEquiv_trans, DoubleCoset.eq, Ideal.Quotient.ker_stabilizerHom, MonoidHom.ker_eq_bot_iff, mem_closure_isSwap', DomMulAct.stabilizerMulEquiv_apply, GrpCat.SurjectiveOfEpiAuxs.h_apply_fromCoset, finEquivZPowers_apply, QuotientGroup.comap_map_mk', MonoidHom.rangeRestrict_injective_iff, Subgroup.center_le_centralizer, Subgroup.goursatFst_prod_goursatSnd_le, Subgroup.inv_subset_closure, cosetToCuspOrbit_apply_mk, MonoidHom.ker_prod, CategoryTheory.PreGaloisCategory.has_decomp_quotients, Group.isNilpotent_top, MulAction.stabilizerEquivStabilizer_one, ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply, Subgroup.index_eq_two_iff_exists_notMem_and, LinearOrderedCommGroup.genLTOne_eq_of_top, Subgroup.index_eq_card, alternatingGroup.isSimpleGroup_five, Equiv.Perm.OnCycleFactors.mem_range_toPermHom_iff, Subgroup.Normal.of_map_subtype, AddMonoidHom.coe_toMultiplicative_map, Subgroup.isSimpleGroup_iff, IsDedekindDomain.selmerGroup.fromUnitLift_injective, Subgroup.unop_injective, alternatingGroup.isCoatom_stabilizer, Subgroup.relIndex_dvd_two_iff, fixedPoints_subgroup_sup, NumberField.Units.logEmbeddingQuot_injective, Subgroup.centralizer_le, isApproximateSubgroup_one, fixedPoints_subgroup_antitone, QuotientGroup.rightRel_eq_top, OpenSubgroup.toSubgroup_injective, cyclotomicCharacter.toZModPow_toFun, ValuationSubring.coe_unitGroupMulEquiv_symm_apply, Subgroup.sup_normal, NumberField.InfinitePlace.isUnramified_iff_stabilizer_eq_bot, MonoidWithZeroHom.valueMonoid_eq_valueGroup', Matrix.mem_glpos, Equiv.Perm.OnCycleFactors.kerParam_range_eq_centralizer_of_count_le_one, Subgroup.toAddSubgroup_comap, Group.fg_iff', Subgroup.coe_eq_univ, Subgroup.le_adjoinNegOne, Ideal.torsionMapQuot_injective, groupHomology.H1CoresCoinfOfTrivial_f, Subgroup.index_eq_two_iff', Subgroup.zpow_mem_zpowers, lowerCentralSeries_nilpotencyClass, ProfiniteGrp.instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemSubgroupLimitConePtAux, MulAction.stabilizerEquivStabilizer_symm, Equiv.Perm.IsCycle.zpowersEquivSupport_symm_apply, MulArchimedeanClass.ballSubgroup_top, MulAction.orbitRel_subgroup_le, orbit_subgroup_eq_rightCoset, image_range_orderOf, Subgroup.inv_mem_iff, OpenNormalSubgroup.toSubgroup_injective, card_zpowers_le, PresentedGroup.closure_range_of, QuotientGroup.measurable_coe, FiniteMulArchimedeanClass.ballSubgroup_strictAnti, IsGaloisGroup.fixingSubgroup_bot, alternatingGroup.exponent_kleinFour_of_card_eq_four, Subgroup.map_comap_le, ModularGroup.coe_one, Sylow.coe_subgroup_smul, mem_nullSubgroup_iff, OpenSubgroup.mem_toSubgroup, Int.subgroup_index_ne_zero_iff, Subgroup.mem_top, Finset.card_pow_quotient_mul_pow_inter_subgroup_le, ModularForm.coe_norm, CongruenceSubgroup.Gamma1_to_Gamma0_mem, IsGaloisGroup.subgroup, isSolvable_iff_commutator_lt, CongruenceSubgroup.mem_conjGL', Ideal.card_stabilizer_eq_card_inertia_mul_finrank, AddSubgroup.coe_toSubgroup_apply, Subgroup.mem_closure, Rep.instPreservesEpimorphismsSubtypeMemSubgroupCoindFunctorSubtype, IsGaloisGroup.intermediateFieldEquivSubgroup_apply, krullTopology_mem_nhds_one_iff, SubMulAction.ofFixingSubgroup_of_singleton_bijective, Equiv.Perm.Basis.ofPermHomFun_apply_of_cycleOf_mem, Equiv.Perm.OnCycleFactors.toPermHom_apply, Finset.card_mul_finset_lt_two, modularCyclotomicCharacter.comp, OpenSubgroup.coe_toSubgroup, Group.closure_finset_fg, Equiv.Perm.isCoatom_stabilizer, Set.powersetCard.isPreprimitive_alternatingGroup, continuousSMul_iff_stabilizer_isOpen, alternatingGroup.instNontrivialSubtypePermFinHAddNatOfNatMemSubgroup, nilpotencyClass_quotient_le, Subgroup.normalClosure_closure_eq_normalClosure, Sylow.normalizer_sup_eq_top, Equiv.Perm.closure_cycle_adjacent_swap, upperCentralSeries_eq_top_iff_nilpotencyClass_le, MonoidHom.finite_iff_finite_ker_range, CommGrpCat.ker_eq_bot_of_mono, lipschitzGroup.coe_mem_iff_mem, IsPGroup.of_bot, MulAction.subgroup_smul_def, Subgroup.normalCore_eq_ker, Subgroup.isComplement'_bot_top, SubMulAction.ofFixingSubgroupEmpty_equivariantMap_bijective, Subgroup.index_eq_one, groupHomology.H1CoresCoinfOfTrivial_g, Subgroup.saturated_iff_zpow, Subgroup.quotientiInfSubgroupOfEmbedding_apply, Subgroup.mem_strictPeriods_iff, MulArchimedeanClass.mem_ballSubgroup_iff, Sylow.dvd_card_of_dvd_card, Subgroup.botCharacteristic, instProperSMulSubtypeMulOppositeMemSubgroupOpOfIsTopologicalGroupOfIsClosedCoe, SubMulAction.fixingSubgroupEquivFixingSubgroup_coe_apply, Representation.toCoinvariants_mk, Subgroup.closure_le_normalClosure, krullTopology_mem_nhds_one_iff_of_normal, Subgroup.mem_map, lowerCentralSeries_zero, CommGroup.primaryComponent.isPGroup, MonoidWithZeroHom.mem_valueGroup_iff_of_comm, Subgroup.subset_normalClosure, Subgroup.toSubmonoid_injective, isCoveringMapOn_quotientMk_of_properlyDiscontinuousSMul, Subgroup.orderIsoCon_symm_apply_coe, QuotientGroup.automorphize_smul_left, Sylow.exists_comap_subtype_eq, IsGalois.map_fixingSubgroup, FiniteMulArchimedeanClass.subgroup_eq_bot, Submonoid.units_iInf₂, Finset.invMulSubgroup_eq_inv_mul, IntermediateField.fixingSubgroup_isOpen, MulArchimedeanClass.subgroup_antitone, Subgroup.le_normalizer_of_normal, ascending_central_series_le_upper, rootsOfUnity_le_of_dvd, MonoidHom.eqLocus_same, Subgroup.val_mem_ofUnits_iff_mem, Subgroup.commProb_subgroup_le, Matrix.SpecialLinearGroup.coe_GLPos_coe_GL_coe_matrix, QuotientGroup.norm_eq_infDist, MonoidHom.ofInjective_apply, MulEquiv.coe_subgroupMap_apply, QuotientGroup.le_norm_iff, MulArchimedeanClass.closedBallSubgroup_top, SubMulAction.mem_fixingSubgroup_union_iff, rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar_val, AddSubgroup.fg_iff_mul_fg, fixingSubgroup_fixedPoints_gc, Subgroup.mem_normalizer_fintype, Subgroup.map_iInf, SubMulAction.map_ofFixingSubgroupUnion_bijective, Subgroup.Commensurable.commensurator'_mem_iff, SubMulAction.of_fixingSubgroupEmpty_mapScalars_surjective, alternatingGroup.commutator_perm_le, QuotientGroup.mk_zpow, Set.mul_subgroupClosure, Subgroup.op_injective, Subgroup.op_sup, NumberField.InfinitePlace.mem_stabilizer_mk_iff, CosetSpace.borelSpace, mem_galBasis_iff, QuotientGroup.measurable_from_quotient, alternatingGroup.isPretransitive_of_three_le_card, SubMulAction.ofFixingSubgroup_of_eq_bijective, Subgroup.unop_sSup, Subgroup.unop_bot, QuotientGroup.orbit_mk_eq_smul, Subgroup.index_top, HNNExtension.ReducedWord.map_fst_eq_and_of_prod_eq, QuotientGroup.instContinuousConstSMul, Equiv.Perm.Basis.ofPermHomFun_mul, eq_cosets_of_normal, Subgroup.mul_mem_iff_of_index_two, Subgroup.transferFunction_apply, rootsOfUnityEquivNthRoots_apply, QuotientGroup.card_preimage_mk, Subgroup.coe_div, Subgroup.ofUnits_injective, Subgroup.normalClosure_idempotent, Rep.resIndAdjunction_unit_app, MulAction.mem_stabilizer_iff, NumberField.IsCMField.indexRealUnits_eq_two_iff, card_rootsOfUnity_eq_iff_exists_isPrimitiveRoot, IsMultiplyPretransitive.alternatingGroup_le, rootsOfUnityCircleEquiv_apply, QuotientGroup.preimage_image_coe, Complex.card_rootsOfUnity, Subgroup.comap_top, IntermediateField.le_iff_le, Subgroup.mem_inv_pointwise_smul_iff, Subgroup.ofUnits_iSup₂, CongruenceSubgroup.conj_cong_is_cong, AddSubgroup.toSubgroup'_closure, MulAction.le_stabilizer_smul_right, Subgroup.IsComplement'.QuotientMulEquiv_symm_apply, InfiniteGalois.fixedField_bot, Subgroup.codisjoint_subgroupOf_sup, SubMulAction.not_mem_of_mem_ofFixingSubgroup, Subgroup.instFiniteQuotientOfContinuousMulOfCompactSpace, alternatingGroup.isMultiplyPretransitive, Subgroup.comap_iInf, DoubleCoset.disjoint_out, Subgroup.subtype_range, SemidirectProduct.mulEquivSubgroup_apply, FiniteMulArchimedeanClass.subsemigroup_eq_subgroup, MonoidHom.coe_range, MulAction.stabilizer_finite, DirichletCharacter.factorsThrough_iff_ker_unitsMap, instProperSMulSubtypeMemSubgroupOfIsClosedCoe, MulAction.stabilizer_inf_stabilizer_le_stabilizer_inter, QuotientGroup.instT1Space, IsPrimitiveRoot.mem_rootsOfUnity, SubMulAction.IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter, MulAction.stabilizer_inf_stabilizer_le_stabilizer_apply₂, NumberField.Units.logEmbeddingEquiv_apply, Subgroup.mem_iff_toUnits_mem_units, Subgroup.closure_preimage_eq_top, NumberField.Units.exist_unique_eq_mul_prod, Equiv.Perm.IsCycle.forall_commute_iff, Subgroup.mem_sup_of_normal_left, Subgroup.mem_normalizer_iff', MulAut.conjNormal_inv_apply, QuotientGroup.monoidHom_ext_iff, Subgroup.unit_of_mem_ofUnits_spec_mem, Subgroup.eq_bot_of_subsingleton, MonoidHom.subgroupMap_surjective, Finset.op_smul_stabilizer_of_no_doubling, MonoidHom.restrict_surjective, QuotientGroup.mk_surjective, MulAction.isMultiplyPreprimitive_ofStabilizer, NumberField.Units.rootsOfUnity_eq_one, Equiv.Perm.stabilizer.surjective_toPerm, Subgroup.mem_toSubmonoid, QuotientGroup.quotientBot_apply, QuotientGroup.isOpenQuotientMap_mk, HNNExtension.NormalWord.TransversalPair.compl, Equiv.Perm.OnCycleFactors.kerParam_range_le_centralizer, autEquivRootsOfUnity_apply_rootOfSplit, HahnSeries.coeff_toOrderTopSubOnePos_pow, ProfiniteGrp.toLimitFun_continuous, IntermediateField.fixedField_bot, SpecialLinearGroup.centerEquivRootsOfUnity_apply_apply, Subgroup.coe_toSubmonoid, DiscreteTiling.PlacedTile.coe_mk_coe, IsZGroup.isCyclic_commutator, SemidirectProduct.mulEquivSubgroup_symm_apply, MulAction.stabilizer_inf_stabilizer_le_stabilizer_union, rootsOfUnity.coe_pow, Subgroup.finite_quotient_of_finite_quotient_of_index_ne_zero, Subgroup.card_le_one_iff_eq_bot, Subgroup.coe_subgroupOf, Equiv.Perm.isCoatom_stabilizer_of_ncard_lt_ncard_compl, Rep.indToCoindAux_snd_mul_inv, QuotientGroup.congr_mk, Subgroup.transferTransversal_apply'', restrictRootsOfUnity_coe_apply, Subgroup.card_subtype, QuotientGroup.preimage_mk_one, Subgroup.ofUnits_sSup, Subgroup.le_centralizer_iff_isMulCommutative, Subgroup.prod_mono_right, IsPrimitiveRoot.zmodEquivZPowers_apply_coe_nat, HasEnoughRootsOfUnity.finite_rootsOfUnity, image_commutatorSet_closureCommutatorRepresentatives, Subgroup.toAddSubgroup'_closure, Subgroup.range_subtype, Equiv.Perm.IsCycle.commute_iff, Ideal.ncard_primesOver_mul_card_inertia_mul_finrank, InfiniteGalois.algEquivToLimit_continuous, Monoid.Coprod.range_eq, Subgroup.coe_op, CommGroup.mem_torsion, Subgroup.closure_union, QuotientGroup.rightRel_eq, NumberField.Units.finiteIndex_iff_sup_torsion_finiteIndex, QuotientGroup.instFirstCountableTopology, commutator_def, upperCentralSeriesStep_eq_comap_center, nilpotencyClass_eq_quotient_center_plus_one, Subgroup.top_subgroupOf, QuotientGroup.map_mk'_self, MulAction.fixingSubgroup_le_stabilizer, IsPrimitiveRoot.val_inv_toRootsOfUnity_coe, DoubleCoset.union_quotToDoubleCoset, Subgroup.exists_pow_mem_of_index_ne_zero, mem_rootsOfUnity', ClassGroup.equiv_mk0, Subgroup.relIndex_pointwise_smul, Equiv.Perm.eq_top_if_isMultiplyPretransitive, Subgroup.ofUnits_right_inverse, MonoidHom.liftOfRightInverse_comp, Subgroup.isComplement_subgroup_right_iff_existsUnique_quotientGroupMk, Subgroup.card_mul_eq_card_subgroup_mul_card_quotient, DoubleCoset.bot_rel_eq_leftRel, mem_fixingSubgroup_iff_subset_fixedBy, MonoidHom.independent_range_of_coprime_order, zpowersEquivZPowers_apply, Matrix.SpecialLinearGroup.discreteSpecialLinearGroupIntRange, Subgroup.normalClosure_eq_self, SubMulAction.mem_ofFixingSubgroup_iff, Equiv.Perm.closure_prime_cycle_swap, SubMulAction.ofStabilizer.conjMap_bijective, rank_closureCommutatorRepresentatives_le, AddSubgroup.index_toSubgroup, Subgroup.topCharacteristic, Group.FG.out, groupHomology.H1CoresCoinfOfTrivial_X₃, MulAction.stabilizerEquivStabilizer_inv, Subgroup.quotientEquivSigmaZMod_symm_apply, Subgroup.mem_prod, mem_fixingSubgroup_iff, SubMulAction.ofFixingSubgroup.isMultiplyPretransitive', MulAction.IwasawaStructure.is_comm, QuotientGroup.ker_le_range_iff, QuotientGroup.mk'_surjective, NumberField.Units.instFiniteIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion, QuotientGroup.equivQuotientZPowOfEquiv_refl, Subgroup.relIndex_ker, MonoidHom.range_le_ker_iff, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, QuotientGroup.mk_mul, Subgroup.mem_zpowers_iff, CategoryTheory.PreGaloisCategory.exists_lift_of_quotient_openSubgroup, IsGalois.tfae, QuotientGroup.image_coe, Subgroup.closure_iUnion, card_rootsOfUnity, Subgroup.equivSMul_symm_apply_coe, Subgroup.smul_toLeftFun, Subgroup.isCyclic, Subgroup.mem_carrier, MonoidWithZeroHom.inv_mem_valueGroup, IsZGroup.isZGroup, QuotientGroup.norm_eq_groupSeminorm, Subgroup.index_map, MonoidHom.subgroupComap_apply_coe, Lagrange.nodal_subgroup_eq_X_pow_card_sub_one, Rep.indToCoindAux_of_not_rel, Subgroup.normal_in_normalizer, coe_powCardSubgroup, ModularGroup.det_coe, FiniteField.sum_subgroup_units, Subgroup.IsComplement'.QuotientMulEquiv_apply, MonoidHom.mem_graph, Subgroup.closure_pow_le, Sylow.instFiniteQuotientSubgroupNormalizerOfFactPrime, isZGroup_iff, ValuationSubring.ker_unitGroupToResidueFieldUnits, HNNExtension.equiv_symm_eq_conj, Subgroup.instNontrivial, Sylow.pow_dvd_card_of_pow_dvd_card, MulChar.apply_mem_rootsOfUnity_orderOf, QuotientGroup.norm_lt_iff, Subgroup.commutator_comm_le, Subgroup.val_finset_prod, IsCyclic.card_powMonoidHom_range, MulAction.aestabilizer_of_aeconst, ModularForm.coe_translate, Equiv.Perm.moves_in, QuotientGroup.equivQuotientZPowOfEquiv_symm, Subgroup.subgroupOf_bot_eq_top, QuotientGroup.mk_prod, Subgroup.isCyclic_iff_exists_zpowers_eq_top, QuotientGroup.comap_comap_center, Subgroup.mem_closure_singleton_self, Subgroup.IsComplement.leftQuotientEquiv_apply, Subgroup.op_eq_bot, QuotientGroup.instLocallyCompactSpace, Subgroup.relIndex_bot_right, Subgroup.card_mul_index, MonoidHom.transfer_eq_pow, MulEquiv.subgroupMap_symm_apply, orbit_subgroup_one_eq_self, stabilizer_isOpen, val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe, Monoid.Coprod.codisjoint_range_inl_range_inr, Subgroup.exists_isComplement_right, Subgroup.commute_subtype_of_commute, GrpCat.epi_iff_range_eq_top, Group.nat_card_center_add_sum_card_noncenter_eq_card, alternatingGroup.card_of_card_eq_four, MonoidHom.ker_one, MulAction.IwasawaStructure.is_conj, ClassGroup.equivPic_apply, DoubleCoset.out_eq', IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_mod_eq, Subgroup.mem_pointwise_smul_iff_inv_smul_mem, Subgroup.le_op_iff, QuotientGroup.instIsTopologicalGroup, Rep.instIsRightAdjointSubtypeMemSubgroupIndFunctorSubtype, QuotientGroup.ker_mk', Subgroup.mem_sup', frattini_nilpotent, Subgroup.normalCore_le, RootPairing.range_weylGroup_weightHom, Subgroup.inf_subgroupOf_left, Sylow.card_eq_card_quotient_normalizer, Subgroup.unop_le_unop_iff, ModularForm.coe_trace, IsGaloisGroup.card_fixingSubgroup_eq_finrank, Subgroup.map_commutator, MulEquiv.symm_comapSubgroup, Subgroup.zpowers_one_eq_bot, Fintype.card_zpowers, AlternatingGroup.map_subtype_of_cycleType, Subgroup.op_sSup, IsGaloisGroup.finrank_fixedPoints_eq_card_subgroup, FiniteMulArchimedeanClass.subgroup_strictAnti, Subgroup.normalizerMonoidHom_apply_symm_apply_coe, Matrix.GLPos.coe_neg_GL, mem_powers_iff_mem_zpowers, MulEquiv.symm_mapSubgroup, groupHomology.H1CoresCoinf_f, Subgroup.ofUnits_iSup, GrpCat.SurjectiveOfEpiAuxs.g_apply_fromCoset, Subgroup.disjoint_iff_mul_eq_one, QuotientGroup.dense_image_mk, Subgroup.index_range, Subgroup.IsSubnormal.lt_normal, MonoidHom.ker_id, QuotientGroup.leftRel_eq_top, Subgroup.bot_prod_bot, Unitization.val_unitsFstOne_mulEquiv_quasiregular_apply, isSimpleGroup_iff, Subgroup.index_map_subtype, MulAction.card_orbit_mul_card_stabilizer_eq_card_group, QuotientGroup.eq_one_iff, Subgroup.mem_unop, Subgroup.centerToMulOpposite_symm_apply_coe, GrpCat.SurjectiveOfEpiAuxs.τ_symm_apply_fromCoset, Equiv.Perm.OnCycleFactors.kerParam_range_eq, Subgroup.closure_eq_bot_iff, Subgroup.coe_comap, autAdjoinRootXPowSubC_root, Subgroup.mem_subgroupOf, CommGrpCat.epi_iff_range_eq_top, Subgroup.smul_bot, nat_card_alternatingGroup, Equiv.Perm.ofSubtype_mem_stabilizer, NumberField.Units.dirichletUnitTheorem.logEmbedding_ker, Subgroup.coe_nonempty, Group.card_center_add_sum_card_noncenter_eq_card, MulAction.IsBlock.subgroup, MulArchimedeanClass.subgroup_eq_bot, Subgroup.mem_inf, Subgroup.dense_xor'_cyclic, Subgroup.Normal.eq_bot_or_eq_top, Subgroup.commProb_quotient_le, ConjClasses.card_carrier, Subgroup.mem_units_iff_val_mem, MonoidHom.ker_snd, Subgroup.instDiscreteTopologyZMultiples, MonoidHom.subgroupMap_apply_coe, Subgroup.IsComplement'.sup_eq_top, NumberField.IsCMField.map_unitsMulComplexConjInv_torsion, CongruenceSubgroup.Gamma_mem, Subgroup.surjOn_iff_le_map, QuotientGroup.strictMono_comap_prod_map, HahnSeries.val_toOrderTopSubOnePos_coe, groupCohomology.H1InfRes_f, lowerCentralSeries_length_eq_nilpotencyClass, Subgroup.commutator_le_left, Subgroup.instNontrivialSubtypeMemTop, Ideal.instNormalSubtypeMemSubgroupStabilizerSubgroupOfInertia, Subgroup.inf_normalizer_le_normalizer_inf, Subgroup.unop_sup, HahnSeries.mem_orderTopSubOnePos_iff, rootsOfUnityEquivNthRoots_symm_apply, SMul.smul_stabilizer_def, Subgroup.norm_coe, ModularGroup.coeHom_apply, IntermediateField.fixingSubgroup_bot, MonoidHom.apply_ofInjective_symm, Subgroup.le_pointwise_smul_iff₀, Subgroup.npow_mem_zpowers, Subgroup.op_le_iff, Subgroup.IsSubnormal.bot, Subgroup.smulCommClass_left, QuotientGroup.quotientBot_symm_apply, HahnSeries.val_inv_toOrderTopSubOnePos_coe, ProfiniteGrp.limit_ext_iff, Subgroup.isLeast_of_closure_iff_eq_mabs, QuotientGroup.mk_div, Unitization.unitsFstOne_val_val_fst, Equiv.Perm.Basis.ofPermHomFun_one, MulAction.minimalPeriod_eq_card, MulAction.mem_stabilizer_finset', QuotientGroup.le_comap_mk', MonoidHom.eqOn_closure, IntermediateField.mem_fixingSubgroup_iff, SubMulAction.ofStabilizer.conjMap_apply, IsPrimitiveRoot.zmodEquivZPowers_apply_coe_int, Subgroup.relIndex_dvd_card, AddSubgroup.toSubgroup_comap, Subgroup.nontrivial_iff_ne_bot, closureCommutatorRepresentatives_fg, InfiniteGalois.fixingSubgroup_isClosed, AddSubgroup.coe_toSubgroup_symm_apply, MulAction.IsBlockSystem.of_normal, Subgroup.isComplement_subgroup_right_iff_bijective, instSubsingletonSubtypeUnitsMemSubgroupRootsOfUnityOfNatNat, nilpotent_quotient_of_nilpotent, IsCyclic.normalizer_le_centralizer, Subgroup.topEquiv_apply, Subgroup.relIndex_top_right, Subgroup.Commensurable.discreteTopology_iff, Subgroup.iSup_eq_closure, MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot, NumberField.IsCMField.complexConj_torsion, MulChar.apply_mem_rootsOfUnity, Subgroup.FG.bot, ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk, instSMulCommClassQuotientSubgroupSubtypeMemSubalgebraSubalgebra, Sylow.mem_fixedPoints_mul_left_cosets_iff_mem_normalizer, Group.IsNilpotent.nilpotent, rootsOfUnityEquivOfPrimitiveRoots_symm_apply, MulAction.ofQuotientStabilizer_smul, Subgroup.IsArithmetic.discreteTopology, Subgroup.commutator_characteristic, AddSubgroup.inertia_map_subtype, Subgroup.Characteristic.comap_quotient_mk, MonoidHom.subgroupComap_surjective_of_surjective, map_rootsOfUnity, commutator_alternatingGroup_eq_self, ClassGroup.mk_def, QuotientGroup.subsingleton_iff, ValuationSubring.coe_unitGroupToResidueFieldUnits_apply, Subgroup.le_normalizer_map, Submonoid.units_mono, nilpotent_iff_finite_ascending_central_series, Subgroup.nat_card_centralizer_nat_card_stabilizer, Subgroup.commutator_bot_left, Subgroup.smul_diff', QuotientGroup.sound, Subgroup.isComplement'_def, Subgroup.commutator_pi_pi_of_finite, SubMulAction.ofFixingSubgroup_insert_map_bijective, modularCyclotomicCharacter.aux_spec, Equiv.Perm.IsThreeCycle.mem_alternatingGroup, Subgroup.IsSubnormal.isSubnormal_iff, Equiv.Perm.OnCycleFactors.kerParam_apply, Subgroup.coe_zpowers, MonoidHom.liftOfRightInverse_comp_apply, AlternatingGroup.card_of_cycleType_mul_eq, Subgroup.mem_bot, Group.fg_range, MulAction.aestabilizer_univ, IntermediateField.fixingSubgroup_sup, Subgroup.IsArithmetic.conj, MulEquiv.subgroupCongr_symm_apply, SlashInvariantForm.coe_norm, groupHomology.mapCycles₁_quotientGroupMk'_epi, Subgroup.instFaithfulSMulSubtypeMem, Subgroup.noncommPiCoprod_range, ZMod.rootsOfUnityAddChar_val, inv_card_commutator_le_commProb, OpenSubgroup.toSubgroup_sup, Subgroup.coe_eq_singleton, MonoidHom.noncommCoprod_injective, Subgroup.ofUnits_sup_units, SubMulAction.conjMap_ofFixingSubgroup_bijective, IsOfFinOrder.powers_eq_zpowers, MonoidHom.coe_ker, IsCancelSMul.stabilizer_eq_bot, commutator_eq_bot_iff_center_eq_top, Subgroup.saturated_iff_npow, MulAction.Quotient.smul_coe, IsZGroup.instQuotientSubgroupOfFinite, Equiv.Perm.nat_card_centralizer, Subgroup.goursat, ValuationSubring.principalUnitGroup_injective, QuotientGroup.instCompactSpaceQuotientSubgroup, Subgroup.comap_subtype, MonoidHom.coe_toAdditive_ker, Subgroup.unop_iInf, Set.subgroupClosure_mul, Abelianization.commutator_subset_ker, rootsOfUnity_zero, modularCyclotomicCharacter.toFun_spec'', NumberField.IsCMField.index_unitsMulComplexConjInv_range_dvd, Subgroup.normal_centralizer, Subgroup.coe_bot, instDiscreteTopologySubtypeGeneralLinearGroupMemSubgroupAdjoinNegOneOfIsTopologicalRingOfT2Space, orbit_fixingSubgroup_compl_subset, QuotientGroup.norm_mk_le_norm, Subgroup.coe_prod, Unitization.mem_unitsFstOne, Subgroup.nilpotencyClass_le, Subgroup.card_eq_iff_eq_top, Subgroup.pointwise_smul_toSubmonoid, Finset.smul_stabilizer_of_no_doubling, Submonoid.mem_units_of_val_mem_inv_val_mem, Subgroup.characteristic_iff_le_map, IsCusp.smul, cyclotomicCharacter.toFun_spec, HNNExtension.ReducedWord.exists_normalWord_prod_eq, SpecialLinearGroup.centerEquivRootsOfUnity_apply_of_finrank_le_one, ClassGroup.equiv_mk, MulAction.mem_stabilizer_finset_iff_subset_smul_finset, Subgroup.orderOf_coe, IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply_toDual, Additive.mem_toAddSubgroup, IsZGroup.instIsCyclicSubtypeMemSubgroupOfFactPrime, Subgroup.val_multiset_prod, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow, IsDedekindDomain.selmerGroup.valuation_ker_eq, Equiv.Perm.OnCycleFactors.range_toPermHom_eq_range_toPermHom', Unitization.unitsFstOne_val_inv_val_fst, ValuationSubring.principalUnitGroup_symm_apply, Subgroup.le_zpowers_iff, NumberField.Units.instFreeIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion, Subgroup.map_inf, Equiv.Perm.OnCycleFactors.centralizer_smul_def, Matrix.SpecialLinearGroup.mem_center_iff, IsSolvable.solvable, Subgroup.mem_closure_iff_of_fintype, MonoidHom.ker_restrict, SubMulAction.IsPretransitive.isPretransitive_ofFixingSubgroup_inter, Subgroup.map_isMulCommutative, Group.exponent_quotient_dvd, Subgroup.subgroupOf_bot_eq_bot, mem_rootsOfUnity_prime_pow_mul_iff, Subgroup.commutator_normal, MulAction.smul_orbit_eq_orbit_smul, Subgroup.relIndex_toAddSubgroup, Subgroup.IsComplement'.disjoint, SubMulAction.conjMap_ofFixingSubgroup_coe_apply, Submodule.unitsQuotEquivRelPic_apply_coe, Subgroup.centralizer_eq_iInf, QuotientGroup.quotientMulEquivOfEq_mk, Equiv.Perm.commute_ofSubtype_noncommPiCoprod, Subgroup.IsSubnormal.exists_chain, Sylow.card_coprime_index, Subgroup.opEquiv_apply, QuotientGroup.t1Space_iff, MonoidHom.coe_toMultiplicative_ker, QuotientGroup.out_conj_pow_minimalPeriod_mem, IsGalois.ofDual_intermediateFieldEquivSubgroup_apply, Sylow.instFiniteSubtypeMemSubgroup, Subgroup.smul_coe, Subgroup.center.isMulCommutative, alternatingGroup.isCoatom_stabilizer_of_ncard_lt_ncard_compl, Subgroup.inf_subgroupOf_inf_normal_of_right, QuotientGroup.leftRel_apply, Equiv.Perm.OnCycleFactors.sign_kerParam_apply_apply, rootsOfUnity.eq_one, Subgroup.MapSubtype.orderIso_symm_apply, Matrix.GLPos.coe_neg, stabilizer_univ_eq_top, CongruenceSubgroup.Gamma0_mem, Rep.quotientToCoinvariantsFunctor_obj_V, AddSubgroup.relIndex_toSubgroup, Subgroup.map_subtype_commutator, Subgroup.card_comap_dvd_of_injective, Subgroup.sup_eq_closure, Subgroup.coe_sInf, Subgroup.isCoatom_comap, autEquivRootsOfUnity_smul, LinearOrderedCommGroup.Subgroup.genLTOne_mem, Group.closure_finite_fg, Subgroup.smul_mem_pointwise_smul_iff, MulAut.conjNormal_apply, Subgroup.Commensurable.equivalence, Subgroup.relIndex_top_left, DoubleCoset.mk_out_eq_mul, Subgroup.unop_top, Subgroup.dense_iff_ne_zpowers
|