| Metric | Count |
|---|
Definitionsclosure, gi, instBot, instCompleteLattice, instInfSet, instInhabited, instMin, instTop, instUniqueOfSubsingleton, instUniqueSubtypeMemBot, toSubgroup, toSubgroup', topEquiv, closure, gi, instBot, instCompleteLattice, instInfSet, instInhabited, instMin, instTop, instUniqueOfSubsingleton, instUniqueSubtypeMemBot, toAddSubgroup, toAddSubgroup', topEquiv | 26 |
Theoremsadd_injective_of_disjoint, add_mem_sup, bot_or_exists_ne_zero, bot_or_nontrivial, bot_toAddSubmonoid, closure_closure_coe_preimage, closure_diff_zero, closure_empty, closure_eq, closure_eq_bot_iff, closure_eq_of_le, closure_eq_top_of_mclosure_eq_top, closure_iUnion, closure_induction, closure_induction₂, closure_insert_zero, closure_le, closure_mono, closure_singleton_zero, closure_union, closure_union_zero, closure_univ, coe_bot, coe_eq_singleton, coe_eq_univ, coe_iInf, coe_iSup_of_directed, coe_inf, coe_sInf, coe_toSubgroup_apply, coe_toSubgroup_symm_apply, coe_top, disjoint_def, disjoint_def', disjoint_iff_add_eq_zero, eq_bot_iff_forall, eq_bot_of_subsingleton, eq_top_iff', exists_mem_sup, exists_ne_zero_of_nontrivial, forall_mem_sup, iSup_eq_closure, instNontrivial, instNontrivialSubtypeMemTop, le_closure_toAddSubmonoid, mem_biSup_of_directedOn, mem_bot, mem_closure, mem_closure_of_mem, mem_closure_pair, mem_closure_singleton, mem_closure_singleton_self, mem_iInf, mem_iSup_of_directed, mem_iSup_of_mem, mem_iSup_prop, mem_inf, mem_sInf, mem_sSup_of_directedOn, mem_sSup_of_mem, mem_sup, mem_sup', mem_sup_left, mem_sup_of_normal_left, mem_sup_of_normal_right, mem_sup_right, mem_toSubgroup', mem_top, ne_bot_iff_exists_ne_zero, nontrivial_iff, nontrivial_iff_exists_ne_zero, nontrivial_iff_ne_bot, notMem_of_notMem_closure, subset_closure, subsingleton_iff, sup_eq_closure, toSubgroup'_closure, toSubgroup_closure, topEquiv_apply, topEquiv_symm_apply_coe, top_toAddSubmonoid, mem_toAddSubgroup, mem_toSubgroup, bot_or_exists_ne_one, bot_or_nontrivial, bot_toSubmonoid, closure_closure_coe_preimage, closure_diff_one, closure_empty, closure_eq, closure_eq_bot_iff, closure_eq_of_le, closure_eq_top_of_mclosure_eq_top, closure_iUnion, closure_induction, closure_induction₂, closure_insert_one, closure_le, closure_mono, closure_singleton_one, closure_union, closure_union_one, closure_univ, coe_bot, coe_eq_singleton, coe_eq_univ, coe_iInf, coe_iSup_of_directed, coe_inf, coe_sInf, coe_toAddSubgroup_apply, coe_toAddSubgroup_symm_apply, coe_top, disjoint_def, disjoint_def', disjoint_iff_mul_eq_one, eq_bot_iff_forall, eq_bot_of_subsingleton, eq_top_iff', exists_mem_sup, exists_ne_one_of_nontrivial, forall_mem_sup, iSup_eq_closure, instNontrivial, instNontrivialSubtypeMemTop, le_closure_toSubmonoid, mem_biSup_of_directedOn, mem_bot, mem_closure, mem_closure_of_mem, mem_closure_pair, mem_closure_singleton, mem_closure_singleton_self, mem_iInf, mem_iSup_of_directed, mem_iSup_of_mem, mem_iSup_prop, mem_inf, mem_sInf, mem_sSup_of_directedOn, mem_sSup_of_mem, mem_sup, mem_sup', mem_sup_left, mem_sup_of_normal_left, mem_sup_of_normal_right, mem_sup_right, mem_toAddSubgroup', mem_top, mul_injective_of_disjoint, mul_mem_sup, ne_bot_iff_exists_ne_one, nontrivial_iff, nontrivial_iff_exists_ne_one, nontrivial_iff_ne_bot, notMem_of_notMem_closure, subset_closure, subsingleton_iff, sup_eq_closure, toAddSubgroup'_closure, toAddSubgroup_closure, topEquiv_apply, topEquiv_symm_apply_coe, top_toSubmonoid | 164 |
| Total | 190 |
| Name | Category | Theorems |
|---|
closure 📖 | CompOp | 88 mathmath: TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure_absorbing, closure_empty, AddGroup.closure_finite_fg, closure_preimage_eq_top, closure_singleton_zero, TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure, closure_diff_zero, mem_closure_range_iff_of_fintype, iSup_eq_closure, closure_nsmul, closure_eq_bot_iff, closure_le_centralizer_centralizer, AddGroup.fg_iff', Int.subgroup_cyclic, mem_closure_of_mem, unop_closure, rank_closure_finset_le_card, AddGroup.fg_iff, closure_singleton_neg, cyclic_of_min, zmultiples_eq_closure, closure_univ, neg_subset_closure, AddMonoidHom.map_closure, centralizer_closure, cyclic_of_isolated_zero, toSubgroup_closure, closure_mono, rank_closure_finite_le_nat_card, AddGroup.rank_spec, Subring.mem_closure_iff, FreeAddGroup.closure_eq_range, fg_iff, op_closure, dense_addSubmonoidClosure_iff_addSubgroupClosure, closure_add_le, closure_toAddSubmonoid, mem_closure_range_iff, closure_addSubmonoidClosure_eq_closure_addSubgroupClosure, mem_closure_singleton_iff_existsUnique_zsmul, closure_image_isAddIndecomposable_baseOf, Submodule.span_int_eq_addSubgroup_closure, Set.nsmul_add_addSubgroupClosure, mem_closure, Submodule.span_int_eq_addSubgroupClosure, topologicalClosure_addSubgroupClosure_toAddSubmonoid, Subgroup.toAddSubgroup_closure, closure_nsmul_le, FreeAddGroup.closure_range_of, AddMonoidHom.eqOn_closure, closure_prod, mem_closure_singleton_self, closure_toAddSubmonoid_of_finite, TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure_nonunital, sup_eq_closure, closure_toAddSubmonoid_of_isOfFinAddOrder, Int.addSubgroupClosure_one, closure_iUnion, dense_addSubgroupClosure_pair_iff, closure_eq, Set.addSubgroupClosure_add, closure_closure_coe_preimage, closure_neg, dense_or_cyclic, AddMonoidHom.closure_preimage_le, AddGroup.closure_finset_fg, closure_insert_zero, NonUnitalSubring.mem_closure_iff, le_closure_toAddSubmonoid, toSubgroup'_closure, AddMonoid.Coprod.closure_range_inl_union_inr, closure_pi, mem_closure_iff_of_fintype, isLeast_of_closure_iff_eq_abs, closure_eq_top_of_mclosure_eq_top, Subgroup.toAddSubgroup'_closure, sup_eq_closure_add, Set.add_addSubgroupClosure, toIntSubmodule_closure, Set.addSubgroupClosure_add_nsmul, mem_closure_singleton, closure_union, mem_closure_pair, closure_le, FreeAddGroup.range_lift_eq_closure, subset_closure, closure_union_zero, Finset.nsmul_right_strictMonoOn
|
gi 📖 | CompOp | — |
instBot 📖 | CompOp | 92 mathmath: closure_empty, ofAddUnits_bot, zero_smul, closure_singleton_zero, ArchimedeanClass.closedBallAddSubgroup_top, bot_toAddSubmonoid, pi_bot, normal_bot, eq_bot_of_card_eq, bot_prod_bot, AddMonoidHom.ker_fst, closure_eq_bot_iff, AddMonoidHom.ker_eq_bot_iff, map_zero_eq_bot, Normal.eq_bot_or_eq_top, isComplement'_top_bot, AddMonoidHom.ker_id, Topology.IsQuotientMap.isCoveringMapOn_of_properlyDiscontinuousVAdd, isComplement'_top_left, ArchimedeanClass.ballAddSubgroup_top, AddMonoidHom.ker_eq_bot_of_cancel, op_bot, AddSubmonoid.addUnits_bot, coe_set_eq_zero, coe_topologicalClosure_bot, pi_eq_bot_iff, AddMonoidHom.ker_snd, AddMonoidHom.range_eq_bot_iff, zmultiples_zero_eq_bot, map_eq_bot_iff, map_eq_bot_iff_of_injective, ArchimedeanClass.addSubgroup_eq_bot, isSimpleAddGroup_iff, card_le_one_iff_eq_bot, isComplement'_top_right, IsSimpleAddGroup.eq_bot_or_eq_top_of_normal, ker_subtype, mem_bot, isSimpleAddGroup_iff, map_bot, unop_eq_bot, coe_bot, IsSubnormal.bot, coe_eq_singleton, unop_bot, eq_bot_or_eq_top_of_prime_card, isCancelVAdd_iff_stabilizer_eq_bot, addSubgroupOf_bot_eq_top, bot_addSubgroupOf, QuotientAddGroup.quotientBot_apply, card_bot, relIndex_bot_right, eq_bot_iff_forall, isComplement'_bot_left, bot_or_nontrivial, botCharacteristic, isCoveringMapOn_quotientMk_of_properlyDiscontinuousVAdd, QuotientAddGroup.quotientBot_symm_apply, addSubgroupOf_bot_eq_bot, Valuation.leAddSubgroup_zero, AddAction.stabilizer_image_coe_quotient, inf_eq_bot_of_coprime, AddMonoidHom.comap_bot, AddMonoidHom.range_zero, AddCommGroup.isAddTorsionFree_iff_torsion_eq_bot, FG.bot, QuotientAddGroup.map_mk'_self, card_eq_one, eq_bot_iff_card, op_eq_bot, bot_or_exists_ne_zero, AddGrpCat.ker_eq_bot_of_mono, addSubgroupOf_eq_bot, RingPreordering.supportAddSubgroup_eq_bot, eq_bot_of_card_le, Topology.IsQuotientMap.isCoveringMapOn_of_vadd_disjoint, prod_eq_bot_iff, isComplement'_bot_top, AddCommGrpCat.ker_eq_bot_of_mono, FiniteArchimedeanClass.addSubgroup_eq_bot, AddCommGrpCat.mono_iff_ker_eq_bot, isComplement'_bot_right, IsCancelVAdd.stabilizer_eq_bot, Submodule.bot_toAddSubgroup, eq_bot_of_subsingleton, zmultiples_eq_bot, index_bot, IsSubnormal.eq_bot_or_top_of_isSimpleAddGroup, relIndex_bot_left, AddGrpCat.mono_iff_ker_eq_bot, ker_inclusion, Bot.isAddCyclic
|
instCompleteLattice 📖 | CompOp | 87 mathmath: map_eq_map_iff, exists_mem_sup, AddMonoidHom.noncommPiCoprod_range, iSup_eq_closure, mem_sup_left, map_eq_range_iff, comap_map_eq, normal_add, add_normal, mem_sup_of_normal_left, noncommPiCoprod_range, relIndex_map_map, coe_iSup_of_directed, mem_iSup_of_directed, relIndex_sup_left, add_mem_sup, mem_sSup_of_directedOn, unop_iSup, mem_sup', disjoint_def, coe_add_of_left_le_normalizer_right, iSupIndep_of_dfinsuppSumAddHom_injective', map_le_map_iff, NumberField.Units.dirichletUnitTheorem.map_logEmbedding_sup_torsion, index_map, AddMonoid.Coprod.range_eq, op_sup, comap_sup_eq_of_le_range, closure_add_le, ofAddUnits_sSup, QuotientAddGroup.comap_map_mk', coe_add_of_right_le_normalizer_left, unop_sup, codisjoint_addSubgroupOf_sup, ofAddUnits_inf, IsSimpleAddGroup.instIsSimpleOrderAddSubgroup, AddMonoid.Coprod.codisjoint_range_inl_range_inr, op_sSup, quotientiInfEmbedding_apply, OpenAddSubgroup.toAddSubgroup_sup, FG.iSup, sup_normal, FG.finset_sup, ofAddUnits_iSup₂, mem_sup_right, sup_eq_closure, instIsModularLatticeAddSubgroup, mem_sup_of_normal_right, FG.biSup_finset, AddMonoid.Coprod.range_lift, closure_iUnion, mem_sup, mem_iSup_of_mem, disjoint_iff_add_eq_zero, mem_sSup_of_mem, quotientiInfAddSubgroupOfEmbedding_apply, mem_iSup_prop, FG.biSup, op_iSup, ofAddUnits_sup_addUnits, fixedPoints_addSubgroup_iSup, comap_sup_eq, disjoint_def', AddMonoidHom.independent_range_of_coprime_order, sup_eq_closure_add, iSup_comap_le, DirectSum.IsInternal.addSubgroup_iSupIndep, unop_sSup, AddMonoid.Coprod.range_inl_sup_range_inr, fixedPoints_addSubgroup_sup, addSubgroupOf_eq_bot, comap_sup_comap_le, map_iSup, FG.sup, ofAddUnits_iSup, closure_union, independent_of_coprime_order, addSubgroupOf_sup, relIndex_sup_right, Submodule.sup_toAddSubgroup, map_sup, iSupIndep_iff_dfinsuppSumAddHom_injective, AddAction.isCoatom_stabilizer_iff_preprimitive, AddAction.IsPreprimitive.isCoatom_stabilizer_of_isPreprimitive, map_le_map_iff', mem_biSup_of_directedOn, normal_addSubgroupOf_sup_of_le_normalizer
|
instInfSet 📖 | CompOp | 28 mathmath: quotientiInfAddSubgroupOfEmbedding_apply_mk, centralizer_eq_iInf, AddSubmonoid.addUnits_iInf₂, AddSubmonoid.addUnits_sInf, index_iInf_le, unop_sInf, op_sInf, fixingAddSubgroup_iUnion, AddSubmonoid.addUnits_iInf, quotientiInfEmbedding_apply_mk, center_eq_infi', quotientiInfEmbedding_apply, finiteIndex_iInf, Subring.sInf_toAddSubgroup, op_iInf, unop_iInf, comap_iInf, coe_iInf, map_iInf, quotientiInfAddSubgroupOfEmbedding_apply, center_eq_iInf, NonUnitalSubring.sInf_toAddSubgroup, mem_sInf, normal_iInf_normal, coe_sInf, finiteIndex_iInf', relIndex_iInf_le, mem_iInf
|
instInhabited 📖 | CompOp | — |
instMin 📖 | CompOp | 40 mathmath: inf_addSubgroupOf_inf_normal_of_left, map_inf_le, inf_addSubgroupOf_left, op_inf, inf_addSubgroupOf_right, AddAction.stabilizer_inf_stabilizer_le_stabilizer_apply₂, relIndex_inf_mul_relIndex, index_inf_le, exists_nsmul_mem_of_relIndex_ne_zero, AddMonoidHom.ker_prod, normal_inf_normal, unop_inf, fixingAddSubgroup_union, map_inf_eq, comap_inf, nsmul_mem_of_relIndex_ne_zero_of_dvd, relIndex_inf_le, addSubgroupOf_map_subtype, inf_add_assoc, map_comap_eq, coe_inf, RingSubgroupsBasis.inter, AddAction.stabilizer_inf_stabilizer_le_stabilizer_inter, AddSubmonoid.addUnits_inf, AddAction.stabilizer_inf_stabilizer_le_stabilizer_union, inf_relIndex_right, ofAddUnits_inf_addUnits, mem_inf, addSubgroupOf_inj, OpenAddSubgroup.toAddSubgroup_inf, add_inf_assoc, map_inf, inf_eq_bot_of_coprime, inf_relIndex_left, inf_addSubgroupOf_inf_normal_of_right, AddAction.stabilizer_inf_stabilizer_le_stabilizer_sdiff, instFiniteIndexMin, AddAction.orbitRel_addSubgroupOf, inf_normalizer_le_normalizer_inf, normal_addSubgroupOf_iff_le_normalizer_inf
|
instTop 📖 | CompOp | 110 mathmath: Int.zmultiples_one, addSubgroupOf_eq_top, closure_preimage_eq_top, pi_top, coe_top, top_addSubgroupOf, instNontrivialSubtypeMemTop, QuotientAddGroup.leftRel_eq_top, addSubgroupOf_self, QuotientAddGroup.subsingleton_quotient_top, card_eq_iff_eq_top, AddMonoidHom.ker_fst, eq_top_of_card_eq, AddAction.aestabilizer_empty, IsSubnormal.lt_normal, AddGroup.fg_iff', AddMonoidHom.range_eq_map, AddAction.aestabilizer_univ, LinearOrderedAddCommGroup.negGen_eq_of_top, Normal.eq_bot_or_eq_top, AddAction.stabilizer_finset_univ, topCharacteristic, AddAction.stabilizer_univ, fixingAddSubgroup_empty, AddGroup.fg_iff, AddAction.stabilizer_empty, map_top_of_surjective, pi_empty, isComplement'_top_bot, MeasureTheory.Lp.boundedContinuousFunction_topologicalClosure, normalizer_eq_top_iff, closure_univ, isComplement'_top_left, map_equiv_top, op_top, Submodule.top_toAddSubgroup, AddGroup.rank_spec, QuotientAddGroup.subsingleton_iff, QuotientAddGroup.rightRel_eq_top, NonUnitalSubring.toAddSubgroup_eq_top, AddCommGrpCat.range_eq_top_of_epi, AddMonoidHom.range_eq_top, AddGroup.FG.out, prod_top, AddMonoidHom.ker_snd, isAddCyclic_iff_exists_zmultiples_eq_top, NormedAddGroupHom.range_comp_incl_top, AddMonoidHom.range_eq_top_of_surjective, IsSubnormal.exists_normal_and_le_and_lt_top_of_ne, AddGroup.fg_def, topEquiv_symm_apply_coe, isComplement'_top_right, IsSimpleAddGroup.eq_bot_or_eq_top_of_normal, top_prod_top, card_top, isSimpleAddGroup_iff, relIndex_top_right, unop_eq_top, QuotientAddGroup.addSubgroup_eq_top_of_subsingleton, FreeAddGroup.closure_range_of, top_toAddSubmonoid, AddCommGrpCat.epi_iff_range_eq_top, eq_top_of_le_card, AddAction.isBlock_top, top_prod, eq_bot_or_eq_top_of_prime_card, addSubgroupOf_bot_eq_top, normalizer_eq_top, AddMonoid.Coprod.range_swap, centralizer_eq_top_iff_subset, Int.addSubgroupClosure_one, eq_top_iff', isComplement'_bot_left, zmultiples_eq_top_of_prime_card, normal_top, closure_closure_coe_preimage, instFiniteIndexTop, topEquiv_apply, OpenAddSubgroup.toAddSubgroup_top, QuotientAddGroup.range_mk', AddGrpCat.epi_iff_range_eq_top, Submodule.toAddSubgroup_eq_top, AddMonoidHom.eqLocus_same, exponent_top, comap_top, AddMonoidHom.ker_eq_top_iff, AddMonoid.Coprod.closure_range_inl_union_inr, Subring.toAddSubgroup_eq_top, unop_top, closure_eq_top_of_mclosure_eq_top, IsSubnormal.iff_eq_top_or_exists, AddAction.stabilizer_finset_empty, AddMonoid.Coprod.range_inl_sup_range_inr, index_top, AddCommGroup.smul_top_eq_top_of_divisibleBy_int, relIndex_top_left, NormedAddGroupHom.ker_zero, AddMonoidHom.range_eq_top_of_cancel, isComplement'_bot_top, coe_eq_univ, AddMonoidHom.ker_zero, isComplement'_bot_right, op_eq_top, AddSubmonoid.addUnits_top, NonUnitalSubring.toAddSubgroup_top, Subring.toAddSubgroup_top, mem_top, index_eq_one, IsSubnormal.eq_bot_or_top_of_isSimpleAddGroup, IsSubnormal.isSubnormal_iff
|
instUniqueOfSubsingleton 📖 | CompOp | — |
instUniqueSubtypeMemBot 📖 | CompOp | — |
toSubgroup 📖 | CompOp | 11 mathmath: MonoidHom.coe_toMultiplicative_range, toSubgroup_closure, Multiplicative.mem_toSubgroup, AddMonoidHom.coe_toMultiplicative_map, coe_toSubgroup_apply, fg_iff_mul_fg, index_toSubgroup, toSubgroup_comap, coe_toSubgroup_symm_apply, MonoidHom.coe_toMultiplicative_ker, relIndex_toSubgroup
|
toSubgroup' 📖 | CompOp | 2 mathmath: mem_toSubgroup', toSubgroup'_closure
|
topEquiv 📖 | CompOp | 2 mathmath: topEquiv_symm_apply_coe, topEquiv_apply
|
| Name | Category | Theorems |
|---|
closure 📖 | CompOp | 111 mathmath: sup_eq_closure_mul, closure_eq, closure_image_isMulIndecomposable_baseOf, closure_prod, Equiv.Perm.closure_isSwap, RootPairing.range_weylGroup_coweightHom, unop_closure, FreeGroup.closure_range_of, closure_toSubmonoid, Equiv.Perm.disjoint_closure_of_disjoint_support, rank_closure_finite_le_nat_card, Finset.pow_right_strictMonoOn, Monoid.Coprod.closure_range_inl_union_inr, MonoidHom.closure_preimage_le, commutator_eq_closure, NumberField.Units.span_basisOfIsMaxRank, closure_le, mem_closure_isSwap, closure_insert_one, Equiv.Perm.closure_isCycle, closure_closure_coe_preimage, Set.subgroupClosure_mul_pow, fg_iff, LinearIsometryEquiv.reflections_generate, AddSubgroup.toSubgroup_closure, centralizer_closure, CoxeterSystem.subgroup_closure_range_simple, closure_empty, Equiv.Perm.closure_cycle_coprime_swap, Group.rank_spec, mem_closure_range_iff_of_fintype, Group.fg_iff, mem_closure_singleton, closure_singleton_one, closure_singleton_inv, mem_closure_range_iff, mem_lowerCentralSeries_succ_iff, NumberField.Units.regOfFamily_div_regulator, FreeGroup.range_lift_eq_closure, closure_mono, rank_closure_finset_le_card, NumberField.IsCMField.closure_realFundSystem_sup_torsion, SpecialLinearGroup.SL2Z_generators, swap_mem_closure_isSwap, NumberField.Units.closure_fundSystem_sup_torsion_eq_top, dense_or_cyclic, FreeGroup.closure_eq_range, MonoidHom.map_closure, Set.pow_mul_subgroupClosure, topologicalClosure_subgroupClosure_toSubmonoid, le_closure_toSubmonoid, closure_le_centralizer_centralizer, closure_eq_top_of_mclosure_eq_top, commutator_def, toAddSubgroup_closure, subset_closure, RootPairing.range_weylGroupToPerm, smul_closure, closure_pi, mem_closure_of_mem, closure_univ, lowerCentralSeries_succ, dense_submonoidClosure_iff_subgroupClosure, closure_submonoidClosure_eq_closure_subgroupClosure, mem_closure_singleton_iff_existsUnique_zpow, Equiv.Perm.swap_mul_swap_same_mem_closure_three_cycles, mem_closure_pair, closure_of_isSwap_of_isPretransitive, Equiv.Perm.IsSwap.mul_mem_closure_three_cycles, MonoidWithZeroHom.valueGroup_def, closure_mul_le, mem_closure_isSwap', inv_subset_closure, Group.fg_iff', PresentedGroup.closure_range_of, mem_closure, Group.closure_finset_fg, normalClosure_closure_eq_normalClosure, Equiv.Perm.closure_cycle_adjacent_swap, closure_inv, cyclic_of_isolated_one, closure_le_normalClosure, op_closure, Set.mul_subgroupClosure, AddSubgroup.toSubgroup'_closure, closure_preimage_eq_top, NumberField.Units.isMaxRank_iff_closure_finiteIndex, toAddSubgroup'_closure, closure_union, Equiv.Perm.closure_prime_cycle_swap, closure_iUnion, closure_pow_le, closure_pow, mem_closure_singleton_self, RootPairing.range_weylGroup_weightHom, closure_eq_bot_iff, Equiv.Perm.closure_cycleType_eq_2_2_eq_alternatingGroup, cyclic_of_min, isLeast_of_closure_iff_eq_mabs, MonoidHom.eqOn_closure, closure_diff_one, iSup_eq_closure, closure_union_one, closure_toSubmonoid_of_isOfFinOrder, zpowers_eq_closure, Equiv.Perm.closure_three_cycles_eq_alternating, closure_toSubmonoid_of_finite, Set.subgroupClosure_mul, mem_closure_iff_of_fintype, sup_eq_closure, Group.closure_finite_fg
|
gi 📖 | CompOp | — |
instBot 📖 | CompOp | 127 mathmath: CongruenceSubgroup.Gamma_zero_bot, MonoidHom.comap_bot, ofUnits_bot, isComplement'_top_left, alternatingGroup.eq_bot_of_card_le_two, IsGaloisGroup.fixingSubgroup_top, op_bot, map_one_eq_bot, Submonoid.units_bot, pi_bot, unop_eq_bot, NumberField.InfinitePlace.IsUnramified.stabilizer_eq_bot, Bot.isCyclic, Matrix.SpecialLinearGroup.center_eq_bot_of_subsingleton, card_eq_one, card_bot, bot_or_nontrivial, DoubleCoset.left_bot_eq_left_quot, GrpCat.mono_iff_ker_eq_bot, IntermediateField.fixingSubgroup_top, normal_bot, rootsOfUnity_one, upperCentralSeries_zero, DoubleCoset.right_bot_eq_right_quot, eq_bot_iff_card, MonoidHom.range_one, isComplement'_bot_right, MonoidHom.range_eq_bot_iff, alternatingGroup.center_eq_bot, isCancelSMul_iff_stabilizer_eq_bot, GrpCat.ker_eq_bot_of_mono, least_descending_central_series_length_eq_nilpotencyClass, CommGroup.isMulTorsionFree_iff_torsion_eq_bot, ker_subtype, closure_empty, prod_eq_bot_iff, NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul_stabilizer, subgroupOf_eq_bot, nilpotent_iff_lowerCentralSeries, pi_eq_bot_iff, isComplement'_top_right, ker_inclusion, bot_or_exists_ne_one, closure_singleton_one, IsGaloisGroup.fixedPoints_bot, relIndex_bot_left, map_eq_bot_iff, DoubleCoset.rel_bot_eq_right_group_rel, DihedralGroup.center_eq_bot_of_odd_ne_one, commutator_eq_bot_iff_le_centralizer, map_bot, Sylow.commutator_eq_bot_or_commutator_eq_self, IsPGroup.bot_lt_center, IsSubnormal.eq_bot_or_top_of_isSimpleGroup, index_bot, commutator_bot_right, IsPGroup.commutator_eq_bot_or_commutator_eq_self, Module.stabilizer_units_eq_bot_of_ne_zero, map_eq_bot_iff_of_injective, isComplement'_bot_left, bot_toSubmonoid, CommGrpCat.mono_iff_ker_eq_bot, lowerCentralSeries_eq_bot_iff_nilpotencyClass_le, Topology.IsQuotientMap.isCoveringMapOn_of_smul_disjoint, isSolvable_def, eq_bot_or_eq_top_of_prime_card, Topology.IsQuotientMap.isCoveringMapOn_of_properlyDiscontinuousSMul, SpecialLinearGroup.center_eq_bot_of_finrank_le_one, MonoidHom.ker_eq_bot_of_cancel, eq_bot_iff_forall, MonoidHom.ker_fst, nilpotent_iff_finite_descending_central_series, bot_subgroupOf, coe_topologicalClosure_bot, MulAction.stabilizer_image_coe_quotient, coe_set_eq_one, isComplement'_top_bot, zpowers_eq_bot, IsSimpleGroup.eq_bot_or_eq_top_of_normal, MonoidHom.ker_eq_bot_iff, isSimpleGroup_iff, NumberField.InfinitePlace.isUnramified_iff_stabilizer_eq_bot, lowerCentralSeries_nilpotencyClass, MulArchimedeanClass.ballSubgroup_top, CommGrpCat.ker_eq_bot_of_mono, IsPGroup.of_bot, isComplement'_bot_top, botCharacteristic, isCoveringMapOn_quotientMk_of_properlyDiscontinuousSMul, FiniteMulArchimedeanClass.subgroup_eq_bot, eq_bot_of_card_eq, MulArchimedeanClass.closedBallSubgroup_top, eq_bot_of_card_le, unop_bot, eq_bot_of_subsingleton, QuotientGroup.quotientBot_apply, IntermediateField.fixedField_bot, card_le_one_iff_eq_bot, QuotientGroup.map_mk'_self, DoubleCoset.bot_rel_eq_leftRel, FiniteField.sum_subgroup_units, subgroupOf_bot_eq_top, op_eq_bot, relIndex_bot_right, zpowers_one_eq_bot, MonoidHom.ker_id, bot_prod_bot, isSimpleGroup_iff, closure_eq_bot_iff, smul_bot, MulArchimedeanClass.subgroup_eq_bot, Normal.eq_bot_or_eq_top, MonoidHom.ker_snd, lowerCentralSeries_length_eq_nilpotencyClass, inf_eq_bot_of_coprime, IsSubnormal.bot, QuotientGroup.quotientBot_symm_apply, lowerCentralSeries_succ_eq_bot, FG.bot, commutator_bot_left, mem_bot, coe_eq_singleton, IsCancelSMul.stabilizer_eq_bot, commutator_eq_bot_iff_center_eq_top, coe_bot, IsSolvable.solvable, subgroupOf_bot_eq_bot
|
instCompleteLattice 📖 | CompOp | 118 mathmath: sup_eq_closure_mul, exists_mem_sup, MulAction.IwasawaStructure.is_generator, MonoidHom.ker_transferSylow_disjoint, Monoid.Coprod.range_inl_sup_range_inr, fixedPoints_subgroup_iSup, map_sup, normalCore_eq_iSup, op_iSup, Equiv.Perm.disjoint_of_disjoint_support, mem_biSup_of_directedOn, map_eq_map_iff, isCoatom_map, mem_iSup_of_mem, mul_normal, coe_mul_of_left_le_normalizer_right, Sylow.normalizer_sup_eq_top', FG.biSup, map_iSup, Equiv.Perm.disjoint_closure_of_disjoint_support, disjoint_rootsOfUnity_of_coprime, normal_subgroupOf_sup_of_le_normalizer, alternatingGroup.isCoatom_stabilizer_singleton, MonoidHom.noncommCoprod_range, IsComplement'.isCompl, mem_iSup_prop, FG.finset_sup, mem_sSup_of_directedOn, FG.biSup_finset, comap_sup_eq, MulAction.isCoatom_stabilizer_iff_preprimitive, Monoid.CoprodI.range_eq_iSup, IsSimpleGroup.instIsSimpleOrderSubgroup, relIndex_map_map, subgroupOf_eq_bot, MulAction.IsPreprimitive.isCoatom_stabilizer_of_isPreprimitive, mem_sup_of_normal_right, relIndex_sup_right, IsPGroup.to_sup_of_normal_left', mem_sup_left, instIsModularLatticeSubgroup, NumberField.Units.regOfFamily_div_regulator, disjoint_def', iSup_comap_le, NumberField.IsCMField.closure_realFundSystem_sup_torsion, FG.sup, disjoint_def, subgroupOf_sup, comap_sup_comap_le, ofUnits_inf, mem_sSup_of_mem, NumberField.Units.closure_fundSystem_sup_torsion_eq_top, IsPGroup.to_sup_of_normal_right, map_le_map_iff, normal_mul, coe_iSup_of_directed, comap_map_eq, mem_sup, Monoid.Coprod.range_lift, IsPGroup.disjoint_of_ne, map_le_map_iff', independent_of_coprime_order, sup_subgroupOf_eq, IsPGroup.le_or_disjoint_of_coprime, quotientiInfEmbedding_apply, mul_mem_sup, smul_sup, map_eq_range_iff, MonoidHom.noncommPiCoprod_range, comap_sup_eq_of_le_range, relIndex_sup_left, FG.iSup, unop_iSup, closure_mul_le, mem_iSup_of_directed, isComplement'_iff_card_mul_and_disjoint, QuotientGroup.comap_map_mk', alternatingGroup.isCoatom_stabilizer, IsPGroup.to_sup_of_normal_right', fixedPoints_subgroup_sup, sup_normal, Equiv.Perm.isCoatom_stabilizer, Sylow.normalizer_sup_eq_top, quotientiInfSubgroupOfEmbedding_apply, op_sup, unop_sSup, ofUnits_iSup₂, codisjoint_subgroupOf_sup, coe_mul_of_right_le_normalizer_left, SemidirectProduct.mulEquivSubgroup_apply, mem_sup_of_normal_left, SemidirectProduct.mulEquivSubgroup_symm_apply, Equiv.Perm.isCoatom_stabilizer_of_ncard_lt_ncard_compl, ofUnits_sSup, Monoid.Coprod.range_eq, closure_union, NumberField.Units.finiteIndex_iff_sup_torsion_finiteIndex, MonoidHom.independent_range_of_coprime_order, IsPGroup.to_sup_of_normal_left, closure_iUnion, index_map, Monoid.Coprod.codisjoint_range_inl_range_inr, mem_sup_right, mem_sup', op_sSup, ofUnits_iSup, disjoint_iff_mul_eq_one, IsComplement'.sup_eq_top, unop_sup, iSup_eq_closure, noncommPiCoprod_range, OpenSubgroup.toSubgroup_sup, MonoidHom.noncommCoprod_injective, ofUnits_sup_units, IsComplement'.disjoint, alternatingGroup.isCoatom_stabilizer_of_ncard_lt_ncard_compl, sup_eq_closure, isCoatom_comap
|
instInfSet 📖 | CompOp | 30 mathmath: Submonoid.units_iInf, Set.unit_eq, op_iInf, finiteIndex_iInf, mem_iInf, ProfiniteGrp.closedSubgroup_eq_sInf_open, normalCore_eq_iInf_conjAct, normal_iInf_normal, index_iInf_le, Submonoid.units_sInf, normalClosure_eq_iInf, quotientiInfSubgroupOfEmbedding_apply_mk, unop_sInf, coe_iInf, finiteIndex_iInf', op_sInf, relIndex_iInf_le, quotientiInfEmbedding_apply_mk, mem_sInf, quotientiInfEmbedding_apply, fixingSubgroup_iUnion, quotientiInfSubgroupOfEmbedding_apply, Submonoid.units_iInf₂, map_iInf, center_eq_infi', center_eq_iInf, comap_iInf, unop_iInf, centralizer_eq_iInf, coe_sInf
|
instInhabited 📖 | CompOp | — |
instMin 📖 | CompOp | 51 mathmath: fixingSubgroup_union, unop_inf, inf_relIndex_left, subgroupOf_inj, map_inf_eq, IsArithmetic.inter, map_comap_eq, MulAction.stabilizer_inf_stabilizer_le_stabilizer_sdiff, instHasDetOneMinGeneralLinearGroup_1, map_inf_le, exists_pow_mem_of_relIndex_ne_zero, instFiniteIndexMin, op_inf, normal_subgroupOf_iff_le_normalizer_inf, index_inf_le, inf_subgroupOf_inf_normal_of_left, normal_inf_normal, OpenSubgroup.toSubgroup_inf, IsPGroup.to_inf_left, inf_relIndex_right, inf_subgroupOf_right, comap_inf, relIndex_inf_mul_relIndex, instHasDetOneMinGeneralLinearGroup, Submonoid.units_inf, subgroupOf_map_subtype, ofUnits_inf_units, Monoid.PushoutI.inf_of_range_eq_base_range, commutator_le_inf, rootsOfUnity_inf_rootsOfUnity, MulAction.orbitRel_subgroupOf, coe_inf, relIndex_inf_le, smul_inf, MonoidHom.ker_prod, mul_inf_assoc, IsPGroup.to_inf_right, inf_mul_assoc, pow_mem_of_relIndex_ne_zero_of_dvd, MulAction.stabilizer_inf_stabilizer_le_stabilizer_inter, MulAction.stabilizer_inf_stabilizer_le_stabilizer_apply₂, IsPGroup.inf_normalizer_sylow, MulAction.stabilizer_inf_stabilizer_le_stabilizer_union, inf_subgroupOf_left, mem_inf, inf_normalizer_le_normalizer_inf, inf_eq_bot_of_coprime, AddSubgroup.inertia_map_subtype, IntermediateField.fixingSubgroup_sup, map_inf, inf_subgroupOf_inf_normal_of_right
|
instTop 📖 | CompOp | 164 mathmath: isComplement'_top_left, MulAction.IwasawaStructure.is_generator, zpowers_eq_top_of_prime_card, NumberField.IsCMField.zpowers_complexConj_eq_top, ZMod.rootsOfUnity_eq_top, Monoid.Coprod.range_inl_sup_range_inr, eq_top_of_card_eq, isCyclic_iff_exists_zpowers_eq_top, normalClosure_of_stabilizer_eq_top, card_top, Group.isNilpotent_iff, Equiv.Perm.closure_isSwap, IsGaloisGroup.fixedPoints_top, fixingSubgroup_empty, subgroupOf_eq_top, Group.fg_def, FreeGroup.closure_range_of, derivedSeries_zero, IsSubnormal.iff_eq_top_or_exists, CommGroup.center_eq_top, subgroupOf_self, OpenSubgroup.toSubgroup_top, Sylow.normalizer_sup_eq_top', MonoidHom.ker_eq_top_iff, alternatingGroup.normalClosure_swap_mul_swap_five, pi_top, MulAction.isBlock_top, op_top, Monoid.Coprod.closure_range_inl_union_inr, Group.IsNilpotent.nilpotent', least_ascending_central_series_length_eq_nilpotencyClass, IsSolvable.commutator_lt_top_of_nontrivial, top_prod, map_top_of_surjective, IsSubnormal.exists_normal_and_le_and_lt_top_of_ne, map_equiv_top, MonoidHom.range_eq_map, CommRing.relPic_eq_top, Equiv.Perm.closure_isCycle, closure_closure_coe_preimage, alternatingGroup.normalClosure_finRotate_five, CongruenceSubgroup.Gamma_one_top, top_toSubmonoid, isComplement'_bot_right, top_fixedByFinite, pi_empty, centralizer_eq_top_iff_subset, normal_top, LinearIsometryEquiv.reflections_generate, upperCentralSeries_nilpotencyClass, CoxeterSystem.subgroup_closure_range_simple, QuotientGroup.subgroup_eq_top_of_subsingleton, stabilizer_empty_eq_top, normalizer_eq_top, MulAction.stabilizer_finset_univ, coe_top, Equiv.Perm.closure_cycle_coprime_swap, Group.rank_spec, Monoid.Coprod.range_swap, Group.fg_iff, isComplement'_top_right, instFiniteIndexTop, MulAction.stabilizer_finset_empty, Submonoid.units_top, mem_lowerCentralSeries_succ_iff, Equiv.Perm.eq_top_of_isPreprimitive_of_isSwap_mem, topEquiv_symm_apply_coe, SpecialLinearGroup.SL2Z_generators, MulAction.stabilizer_univ, MulAction.stabilizer_empty, IsSubnormal.eq_bot_or_top_of_isSimpleGroup, NumberField.Units.closure_fundSystem_sup_torsion_eq_top, top_prod_top, CommGrpCat.range_eq_top_of_epi, Equiv.Perm.subgroup_eq_top_of_isPreprimitive_of_isSwap_mem, exponent_top, eq_top_iff', closure_eq_top_of_mclosure_eq_top, alternatingGroup.subgroup_eq_top_of_isPreprimitive, CongruenceSubgroup.finiteIndex_conjGL, QuotientGroup.range_mk', MonoidHom.range_eq_top, op_eq_top, isComplement'_bot_left, MulAction.aestabilizer_empty, closure_univ, eq_bot_or_eq_top_of_prime_card, IsZGroup.commutator_lt, IsGalois.fixedField_top, lowerCentralSeries_succ, QuotientGroup.subsingleton_quotient_top, normalizerCondition_iff_only_full_group_self_normalizing, prod_top, ClassGroup.equivPic_symm_apply, Equiv.Perm.eq_top_of_isMultiplyPretransitive, commutator_alternatingGroup_eq_top, Equiv.Perm.subgroup_eq_top_of_swap_mem, MonoidHom.range_eq_top_of_surjective, MonoidHom.ker_fst, closure_of_isSwap_of_isPretransitive, isComplement'_top_bot, MonoidHom.range_eq_top_of_cancel, unop_eq_top, Equiv.Perm.IsThreeCycle.alternating_normalClosure, normalizer_eq_top_iff, IsSimpleGroup.eq_bot_or_eq_top_of_normal, Equiv.Perm.subgroup_eq_top_of_nontrivial, Group.isNilpotent_top, LinearOrderedCommGroup.genLTOne_eq_of_top, QuotientGroup.rightRel_eq_top, Group.fg_iff', coe_eq_univ, PresentedGroup.closure_range_of, IsGaloisGroup.fixingSubgroup_bot, mem_top, Sylow.normalizer_sup_eq_top, Equiv.Perm.closure_cycle_adjacent_swap, upperCentralSeries_eq_top_iff_nilpotencyClass_le, isComplement'_bot_top, index_eq_one, lowerCentralSeries_zero, MonoidHom.eqLocus_same, index_top, NumberField.IsCMField.indexRealUnits_eq_two_iff, comap_top, InfiniteGalois.fixedField_bot, SemidirectProduct.mulEquivSubgroup_apply, closure_preimage_eq_top, SemidirectProduct.mulEquivSubgroup_symm_apply, commutator_def, top_subgroupOf, Equiv.Perm.eq_top_if_isMultiplyPretransitive, Equiv.Perm.closure_prime_cycle_swap, topCharacteristic, Group.FG.out, IsGalois.tfae, MulAction.aestabilizer_of_aeconst, subgroupOf_bot_eq_top, GrpCat.epi_iff_range_eq_top, MonoidHom.ker_one, IsSubnormal.lt_normal, QuotientGroup.leftRel_eq_top, isSimpleGroup_iff, CommGrpCat.epi_iff_range_eq_top, Normal.eq_bot_or_eq_top, MonoidHom.ker_snd, IsComplement'.sup_eq_top, instNontrivialSubtypeMemTop, IntermediateField.fixingSubgroup_bot, topEquiv_apply, relIndex_top_right, Group.IsNilpotent.nilpotent, QuotientGroup.subsingleton_iff, nilpotent_iff_finite_ascending_central_series, IsSubnormal.isSubnormal_iff, MulAction.aestabilizer_univ, commutator_eq_bot_iff_center_eq_top, rootsOfUnity_zero, card_eq_iff_eq_top, eq_top_of_le_card, IsSubnormal.exists_chain, stabilizer_univ_eq_top, relIndex_top_left, unop_top
|
instUniqueOfSubsingleton 📖 | CompOp | — |
instUniqueSubtypeMemBot 📖 | CompOp | — |
toAddSubgroup 📖 | CompOp | 14 mathmath: NumberField.Units.span_basisOfIsMaxRank, fg_iff_add_fg, NumberField.Units.dirichletUnitTheorem.map_logEmbedding_sup_torsion, MonoidHom.coe_toAdditive_map, coe_toAddSubgroup_symm_apply, toAddSubgroup_closure, coe_toAddSubgroup_apply, index_toAddSubgroup, MonoidHom.coe_toAdditive_range, toAddSubgroup_comap, NumberField.Units.dirichletUnitTheorem.logEmbedding_ker, MonoidHom.coe_toAdditive_ker, Additive.mem_toAddSubgroup, relIndex_toAddSubgroup
|
toAddSubgroup' 📖 | CompOp | 2 mathmath: mem_toAddSubgroup', toAddSubgroup'_closure
|
topEquiv 📖 | CompOp | 3 mathmath: topEquiv_symm_apply_coe, ClassGroup.equivPic_symm_apply, topEquiv_apply
|