| Metric | Count |
|---|
DefinitionsIsFiniteRelIndex, fintypeOfIndexNeZero, fintypeQuotientOfFiniteIndex, index, relIndex, IsFiniteRelIndex, fintypeOfIndexNeZero, fintypeQuotientOfFiniteIndex, index, relIndex | 10 |
Theoremsindex_stabilizer, index_stabilizer_of_transitive, card_fiber_eq_of_mem_range, finite_iff_finite_ker_range, surjective_of_card_ker_le_div, index_ne_zero, relIndex_ne_zero, to_finiteIndex_addSubgroupOf, add_mem_iff_of_index_two, add_self_mem_of_index_two, card_dvd_of_surjective, card_eq_one, card_map_dvd, card_mul_index, card_range_dvd, dvd_index_map, exists_nsmul_mem_of_index_ne_zero, exists_nsmul_mem_of_relIndex_ne_zero, finiteIndex_iInf, finiteIndex_iInf', finiteIndex_iff, finiteIndex_iff_finite_quotient, finiteIndex_ker, finiteIndex_of_finite, finiteIndex_of_finite_quotient, finiteIndex_of_le, finite_iff_finite_and_finiteIndex, finite_quotient_of_finiteIndex, finite_quotient_of_finite_quotient_of_index_ne_zero, finite_quotient_of_pretransitive_of_index_ne_zero, index_antitone, index_bot, index_comap, index_comap_of_surjective, index_dvd_card, index_dvd_of_le, index_dvd_two_iff, index_dvd_two_iff', index_eq_card, index_eq_one, index_eq_two_iff, index_eq_two_iff', index_eq_two_iff_exists_notMem_and, index_eq_two_iff_exists_notMem_and', index_eq_zero_iff_infinite, index_eq_zero_of_relIndex_eq_zero, index_iInf_le, index_iInf_ne_zero, index_inf_le, index_inf_ne_zero, index_ker, index_map, index_map_dvd, index_map_eq, index_map_equiv, index_map_of_bijective, index_map_of_injective, index_map_subtype, index_mul_card, index_ne_zero_iff_finite, index_ne_zero_of_finite, index_pi, index_prod, index_range, index_smul, index_strictAnti, index_toSubgroup, index_top, inf_eq_bot_of_coprime, inf_relIndex_left, inf_relIndex_right, instFiniteIndexMin, instFiniteIndexTop, instFiniteIndex_addSubgroupOf, not_finiteIndex_iff, nsmul_mem_of_index_ne_zero_of_dvd, nsmul_mem_of_relIndex_ne_zero_of_dvd, one_lt_index_of_ne_top, relIindex_dvd_two_iff', relIindex_eq_two_iff', relIndex_addSubgroupOf, relIndex_bot_left, relIndex_bot_right, relIndex_comap, relIndex_comap_ne_zero, relIndex_dvd_card, relIndex_dvd_index_of_le, relIndex_dvd_index_of_normal, relIndex_dvd_of_le_left, relIndex_dvd_two_iff, relIndex_eq_one, relIndex_eq_two_iff, relIndex_eq_two_iff_exists_notMem_and, relIndex_eq_two_iff_exists_notMem_and', relIndex_eq_zero_of_le_left, relIndex_eq_zero_of_le_right, relIndex_iInf_le, relIndex_iInf_ne_zero, relIndex_inf_le, relIndex_inf_mul_relIndex, relIndex_inf_ne_zero, relIndex_inter_ne_zero, relIndex_ker, relIndex_le_of_le_left, relIndex_le_of_le_right, relIndex_map_map, relIndex_map_map_of_injective, relIndex_mul_index, relIndex_mul_relIndex, relIndex_ne_zero, relIndex_ne_zero_trans, relIndex_pointwise_smul, relIndex_self, relIndex_sup_left, relIndex_sup_right, relIndex_toSubgroup, relIndex_top_left, relIndex_top_right, two_smul_mem_of_index_two, card_fiber_eq_of_mem_range, finite_iff_finite_ker_range, surjective_of_card_ker_le_div, index_stabilizer, index_stabilizer_of_transitive, index_ne_zero, relIndex_ne_zero, to_finiteIndex_subgroupOf, card_dvd_of_surjective, card_eq_one, card_map_dvd, card_mul_index, card_range_dvd, dvd_index_map, exists_pow_mem_of_index_ne_zero, exists_pow_mem_of_relIndex_ne_zero, finiteIndex_iInf, finiteIndex_iInf', finiteIndex_iff, finiteIndex_iff_finite_quotient, finiteIndex_ker, finiteIndex_normalCore, finiteIndex_of_finite, finiteIndex_of_finite_quotient, finiteIndex_of_le, finite_iff_finite_and_finiteIndex, finite_quotient_of_finiteIndex, finite_quotient_of_finite_quotient_of_index_ne_zero, finite_quotient_of_pretransitive_of_index_ne_zero, index_antitone, index_bot, index_comap, index_comap_of_surjective, index_dvd_card, index_dvd_of_le, index_dvd_two_iff, index_dvd_two_iff', index_eq_card, index_eq_one, index_eq_two_iff, index_eq_two_iff', index_eq_two_iff_exists_notMem_and, index_eq_two_iff_exists_notMem_and', index_eq_zero_iff_infinite, index_eq_zero_of_relIndex_eq_zero, index_iInf_le, index_iInf_ne_zero, index_inf_le, index_inf_ne_zero, index_ker, index_map, index_map_dvd, index_map_eq, index_map_equiv, index_map_of_bijective, index_map_of_injective, index_map_subtype, index_mul_card, index_ne_zero_iff_finite, index_ne_zero_of_finite, index_pi, index_prod, index_range, index_strictAnti, index_toAddSubgroup, index_top, inf_eq_bot_of_coprime, inf_relIndex_left, inf_relIndex_right, instFiniteIndexMin, instFiniteIndexTop, instFiniteIndex_subgroupOf, mul_mem_iff_of_index_two, mul_self_mem_of_index_two, not_finiteIndex_iff, one_lt_index_of_ne_top, pow_mem_of_index_ne_zero_of_dvd, pow_mem_of_relIndex_ne_zero_of_dvd, relIindex_dvd_two_iff', relIindex_eq_two_iff', relIndex_bot_left, relIndex_bot_right, relIndex_comap, relIndex_comap_ne_zero, relIndex_dvd_card, relIndex_dvd_index_of_le, relIndex_dvd_index_of_normal, relIndex_dvd_of_le_left, relIndex_dvd_two_iff, relIndex_eq_one, relIndex_eq_two_iff, relIndex_eq_two_iff_exists_notMem_and, relIndex_eq_two_iff_exists_notMem_and', relIndex_eq_zero_of_le_left, relIndex_eq_zero_of_le_right, relIndex_iInf_le, relIndex_iInf_ne_zero, relIndex_inf_le, relIndex_inf_mul_relIndex, relIndex_inf_ne_zero, relIndex_inter_ne_zero, relIndex_ker, relIndex_le_of_le_left, relIndex_le_of_le_right, relIndex_map_map, relIndex_map_map_of_injective, relIndex_mul_index, relIndex_mul_relIndex, relIndex_ne_zero, relIndex_ne_zero_trans, relIndex_pointwise_smul, relIndex_self, relIndex_subgroupOf, relIndex_sup_left, relIndex_sup_right, relIndex_toAddSubgroup, relIndex_top_left, relIndex_top_right, sq_mem_of_index_two | 238 |
| Total | 248 |