| Metric | Count |
|---|
DefinitionsaddCommGroupTopologicalClosure, connectedComponentOfZero, topologicalClosure, addLeft, addRight, divLeft, divRight, inv, mulLeft, mulRight, neg, prodAddUnits, prodUnits, shearAddRight, shearMulRight, subLeft, subRight, commGroupTopologicalClosure, connectedComponentOfOne, topologicalClosure, nhdsAddHom, nhdsMulHom, toAddUnits_homeomorph, toUnits_homeomorph | 24 |
TheoremscontinuousConstSMul_int, continuousSMul_int, isOpenQuotientMap_of_isQuotientMap, coe_topologicalClosure_bot, instIsTopologicalAddGroupSubtypeMem, isClosed_topologicalClosure, is_normal_topologicalClosure, le_topologicalClosure, properlyDiscontinuousVAdd_of_tendsto_cofinite, properlyDiscontinuousVAdd_opposite_of_tendsto_cofinite, topologicalClosure_coe, topologicalClosure_minimal, instCompactSpaceOfT1SpaceOfContinuousAdd, instIsTopologicalAddGroupOfContinuousAdd, instLocallyCompactSpaceOfT1SpaceOfContinuousAdd, instWeaklyLocallyCompactSpaceOfT1SpaceOfContinuousAdd, isClosedEmbedding_embedProduct, isEmbedding_val, range_embedProduct, units_continuousConstSMul, of_coeHom_comp, of_inv, of_neg, zpow, zsmul, of_inv, of_neg, zpow, zsmul, induced, of_nhds_one, induced, of_nhds_zero, of_inv, of_neg, zpow, zsmul, zpow, zsmul, topologicalClosure_map_addSubgroup, topologicalClosure_map_subgroup, nhds_of_one, nhds_of_zero, const_div', const_sub, div_const', sub_const, zpow, zsmul, inv_nhdsGT, inv_nhdsLT, inv_nhdsNE, map_add_left_nhdsGT, map_add_left_nhdsLT, map_add_left_nhdsNE, map_add_right_nhdsGT, map_add_right_nhdsLT, map_add_right_nhdsNE, map_mul_left_nhdsGT, map_mul_left_nhdsLT, map_mul_left_nhdsNE, map_mul_right_nhdsGT, map_mul_right_nhdsLT, map_mul_right_nhdsNE, neg_nhdsGT, neg_nhdsLT, neg_nhdsNE, tendsto_add_const_iff, tendsto_const_add_iff, tendsto_const_div_iff, tendsto_const_div_iff', tendsto_const_mul_iff, tendsto_const_sub_iff, tendsto_div_const_iff, tendsto_div_const_iff', tendsto_mul_const_iff, tendsto_sub_const_iff, addLeft_symm, addRight_symm, coe_addLeft, coe_addRight, coe_inv, coe_mulLeft, coe_mulRight, coe_neg, divLeft_apply, divLeft_symm_apply, divRight_apply, divRight_symm_apply, mulLeft_symm, mulRight_symm, shearAddRight_coe, shearAddRight_symm_coe, shearMulRight_coe, shearMulRight_symm_coe, subLeft_apply, subLeft_symm_apply, subRight_apply, subRight_symm_apply, symm_inv, symm_neg, inv, neg, zpow, zsmul, inv, leftCoset, left_addCoset, neg, rightCoset, right_addCoset, inv, neg, inv, leftCoset, left_addCoset, neg, rightCoset, right_addCoset, continuous_addConj_prod, continuous_conj, continuous_conj', exists_antitone_basis_nhds_zero, ext, ext_iff, isInducing_iff_nhds_zero, isOpenMap_iff_nhds_zero, of_comm_of_nhds_zero, of_nhds_zero, of_nhds_zero', t1Space, continuous_conj, continuous_conj', continuous_conj_prod, exists_antitone_basis_nhds_one, ext, ext_iff, isInducing_iff_nhds_one, isOpenMap_iff_nhds_one, of_comm_of_nhds_one, of_nhds_one, of_nhds_one', t1Space, isOpenQuotientMap_of_isQuotientMap, instContinuousInv, instContinuousNeg, instIsTopologicalAddGroup, instIsTopologicalGroup, continuousInv, continuousNeg, has_continuous_inv', has_continuous_neg', topologicalAddGroup, topologicalGroup, continuousInv, continuousNeg, instIsTopologicalAddGroup, instIsTopologicalGroup, sigmaCompactSpace, sigmaCompactSpace, isClosed_centralizer, inv, neg, zpow, zsmul, coe_topologicalClosure_bot, instIsTopologicalGroupSubtypeMem, isClosed_topologicalClosure, is_normal_topologicalClosure, le_topologicalClosure, properlyDiscontinuousSMul_of_tendsto_cofinite, properlyDiscontinuousSMul_opposite_of_tendsto_cofinite, topologicalClosure_coe, topologicalClosure_minimal, units_isCompact, isOpenMap_iff_nhds_one, isOpenMap_iff_nhds_zero, continuousInv, continuousNeg, topologicalAddGroup, topologicalGroup, instCompactSpaceOfT1SpaceOfContinuousMul, instIsTopologicalGroupOfContinuousMul, instLocallyCompactSpaceOfT1SpaceOfContinuousMul, instWeaklyLocallyCompactSpaceOfT1SpaceOfContinuousMul, isClosedEmbedding_embedProduct, isEmbedding_val, range_embedProduct, add_mem_connectedComponent_zero, compact_covered_by_add_left_translates, compact_covered_by_mul_left_translates, compact_open_separated_add_left, compact_open_separated_add_right, compact_open_separated_mul_left, compact_open_separated_mul_right, continuousAt_inv, continuousAt_inv_iff, continuousAt_neg, continuousAt_neg_iff, continuousAt_zpow, continuousAt_zsmul, continuousInv_iInf, continuousInv_inf, continuousInv_of_discreteTopology, continuousInv_sInf, continuousNeg_iInf, continuousNeg_inf, continuousNeg_of_discreteTopology, continuousNeg_sInf, continuousOn_inv, continuousOn_inv_iff, continuousOn_neg, continuousOn_neg_iff, continuousOn_zpow, continuousOn_zsmul, continuousWithinAt_inv, continuousWithinAt_neg, continuous_div_left', continuous_div_right', continuous_inv_iff, continuous_neg_iff, continuous_of_continuousAt_one, continuous_of_continuousAt_oneβ, continuous_of_continuousAt_zero, continuous_of_continuousAt_zeroβ, continuous_sub_left, continuous_sub_right, continuous_zpow, continuous_zsmul, discreteTopology_iff_isOpen_singleton_one, discreteTopology_iff_isOpen_singleton_zero, discreteTopology_of_isOpen_singleton_one, discreteTopology_of_isOpen_singleton_zero, exists_disjoint_smul_of_isCompact, exists_disjoint_vadd_of_isCompact, exists_nhds_half_neg, exists_nhds_split_inv, instContinuousInvMulOpposite, instContinuousInvMultiplicativeOfContinuousNeg, instContinuousInvULift, instContinuousNegAddOpposite, instContinuousNegAdditiveOfContinuousInv, instContinuousNegULift, instIsTopologicalAddGroupAddOpposite, instIsTopologicalAddGroupAdditiveOfIsTopologicalGroup, instIsTopologicalGroupMulOpposite, instIsTopologicalGroupMultiplicativeOfIsTopologicalAddGroup, instIsTopologicalGroupULift, inv_closure, inv_mem_connectedComponent_one, inv_mem_nhds_one, isClosedMap_add_left, isClosedMap_add_right, isClosedMap_div_left, isClosedMap_div_right, isClosedMap_inv, isClosedMap_mul_left, isClosedMap_mul_right, isClosedMap_neg, isClosedMap_sub_left, isClosedMap_sub_right, isClosed_setOf_map_inv, isClosed_setOf_map_neg, isOpenMap_add_left, isOpenMap_add_right, isOpenMap_div_left, isOpenMap_div_right, isOpenMap_inv, isOpenMap_mul_left, isOpenMap_mul_right, isOpenMap_neg, isOpenMap_sub_left, isOpenMap_sub_right, map_add_left_nhds, map_add_left_nhds_zero, map_add_right_nhds, map_add_right_nhds_zero, map_mul_left_nhds, map_mul_left_nhds_one, map_mul_right_nhds, map_mul_right_nhds_one, mem_closure_iff_nhds_one, mem_closure_iff_nhds_zero, mul_mem_connectedComponent_one, neg_closure, neg_mem_connectedComponent_zero, neg_mem_nhds_zero, nhdsAddHom_apply, nhdsMulHom_apply, nhds_add, nhds_inv, nhds_mul, nhds_neg, nhds_one_symm, nhds_one_symm', nhds_translation_add_neg, nhds_translation_div, nhds_translation_inv_mul, nhds_translation_mul_inv, nhds_translation_neg_add, nhds_translation_sub, nhds_zero_symm, nhds_zero_symm', tendsto_div_nhds_one_iff, tendsto_inv, tendsto_inv_iff, tendsto_inv_nhdsGE, tendsto_inv_nhdsGE_inv, tendsto_inv_nhdsGT, tendsto_inv_nhdsGT_inv, tendsto_inv_nhdsLE, tendsto_inv_nhdsLE_inv, tendsto_inv_nhdsLT, tendsto_inv_nhdsLT_inv, tendsto_inv_nhdsWithin_Iic_inv, tendsto_neg, tendsto_neg_iff, tendsto_neg_nhdsGE, tendsto_neg_nhdsGE_neg, tendsto_neg_nhdsGT, tendsto_neg_nhdsGT_neg, tendsto_neg_nhdsLE, tendsto_neg_nhdsLE_neg, tendsto_neg_nhdsLT, tendsto_neg_nhdsLT_neg, tendsto_sub_nhds_zero_iff, topologicalAddGroup_iInf, topologicalAddGroup_induced, topologicalAddGroup_inf, topologicalAddGroup_of_discreteTopology, topologicalAddGroup_sInf, topologicalGroup_iInf, topologicalGroup_induced, topologicalGroup_inf, topologicalGroup_of_discreteTopology, topologicalGroup_sInf | 336 |
| Total | 360 |