| Metric | Count |
|---|
| Definitions | 0 |
Theoremsadd_sum_erase, card_biUnion, card_biUnion_le, card_disjiUnion, card_eq_sum_card_fiberwise, card_eq_sum_card_image, card_eq_sum_ones, card_nsmul_add_sum, eq_of_card_le_one_of_prod_eq, eq_of_card_le_one_of_sum_eq, eq_one_of_prod_eq_one, eq_prod_range_div, eq_prod_range_div', eq_sum_range_sub, eq_sum_range_sub', eq_zero_of_sum_eq_zero, eventually_constant_prod, eventually_constant_sum, exists_ne_one_of_prod_ne_one, exists_ne_zero_of_sum_ne_zero, mem_sum, mul_prod_erase, nsmul_eq_sum_const, pow_card_mul_prod, pow_eq_prod_const, prod_attach, prod_biUnion, prod_biUnion_of_pairwise_eq_one, prod_bij_ne_one, prod_cancels_of_partition_cancels, prod_coe_sort, prod_comp, prod_comp_equiv, prod_compl_mul_prod, prod_congr, prod_congr_of_eq_on_inter, prod_congr_set, prod_cons, prod_cons', prod_const, prod_diag, prod_disjSum, prod_disjUnion, prod_disjiUnion, prod_dvd_prod_of_dvd, prod_eq_fold, prod_eq_ite, prod_eq_mul, prod_eq_mul_of_mem, prod_eq_one, prod_eq_one_iff, prod_eq_pow_card, prod_eq_prod_extend, prod_eq_single, prod_eq_single_of_mem, prod_erase, prod_erase_eq_div, prod_erase_lt_of_one_lt, prod_erase_mul, prod_extend_by_one, prod_fiberwise, prod_fiberwise', prod_fiberwise_eq_prod_filter, prod_fiberwise_eq_prod_filter', prod_fiberwise_of_maps_to, prod_fiberwise_of_maps_to', prod_filter, prod_filter_mul_prod_filter_not, prod_filter_ne_one, prod_filter_not_mul_prod_filter, prod_filter_of_ne, prod_filter_of_pairwise_eq_one, prod_filter_xor, prod_finset_coe, prod_flip, prod_image, prod_image', prod_image_of_disjoint, prod_image_of_pairwise_eq_one, prod_insert, prod_insert', prod_insert_div, prod_insert_of_eq_one_if_notMem, prod_insert_one, prod_involution, prod_ite_mem_eq, prod_list_count, prod_list_count_of_subset, prod_list_map_count, prod_map_equiv, prod_mul_distrib, prod_mul_eq_prod_mul_of_exists, prod_mul_pow_card, prod_mul_prod_comm, prod_mul_prod_compl, prod_multiset_count, prod_multiset_count_of_subset, prod_multiset_map_count, prod_ninvolution, prod_of_injOn, prod_pair, prod_partition, prod_pow_eq_pow_sum, prod_range_add, prod_range_add_div_prod_range, prod_range_div, prod_range_div', prod_range_induction, prod_range_one, prod_range_succ, prod_range_succ', prod_range_succ_comm, prod_sdiff, prod_sdiff_div_prod_sdiff, prod_sdiff_eq_div, prod_sdiff_eq_prod_sdiff_iff, prod_sdiff_ne_prod_sdiff_iff, prod_set_coe, prod_singleton, prod_singleton', prod_subset, prod_subset_one_on_sdiff, prod_subtype, prod_subtype_eq_prod_filter, prod_subtype_map_embedding, prod_subtype_of_mem, prod_sumElim, prod_sum_eq_prod_toLeft_mul_prod_toRight, prod_union, prod_union_eq_left, prod_union_eq_right, prod_union_inter, prod_unique_nonempty, sum_add_card_nsmul, sum_add_distrib, sum_add_eq_sum_add_of_exists, sum_add_sum_comm, sum_add_sum_compl, sum_attach, sum_biUnion, sum_biUnion_of_pairwise_eq_zero, sum_bij_ne_zero, sum_cancels_of_partition_cancels, sum_card_fiberwise_eq_card_filter, sum_coe_sort, sum_comp, sum_comp_equiv, sum_compl_add_sum, sum_congr, sum_congr_of_eq_on_inter, sum_congr_set, sum_cons, sum_cons', sum_const, sum_const_nat, sum_diag, sum_disjSum, sum_disjUnion, sum_disjiUnion, sum_eq_add, sum_eq_add_of_mem, sum_eq_card_nsmul, sum_eq_fold, sum_eq_ite, sum_eq_single, sum_eq_single_of_mem, sum_eq_sum_extend, sum_eq_zero, sum_eq_zero_iff, sum_erase, sum_erase_add, sum_erase_eq_sub, sum_erase_lt_of_pos, sum_extend_by_zero, sum_fiberwise, sum_fiberwise', sum_fiberwise_eq_sum_filter, sum_fiberwise_eq_sum_filter', sum_fiberwise_of_maps_to, sum_fiberwise_of_maps_to', sum_filter, sum_filter_add_sum_filter_not, sum_filter_ne_zero, sum_filter_not_add_sum_filter, sum_filter_of_ne, sum_filter_of_pairwise_eq_zero, sum_filter_xor, sum_finset_coe, sum_flip, sum_image, sum_image', sum_image_of_disjoint, sum_image_of_pairwise_eq_zero, sum_insert, sum_insert', sum_insert_of_eq_zero_if_notMem, sum_insert_sub, sum_insert_zero, sum_involution, sum_ite_mem_eq, sum_list_count, sum_list_count_of_subset, sum_list_map_count, sum_map_equiv, sum_multiset_count, sum_multiset_count_of_subset, sum_multiset_map_count, sum_ninvolution, sum_nsmul_assoc, sum_of_injOn, sum_pair, sum_partition, sum_range_add, sum_range_add_sub_sum_range, sum_range_induction, sum_range_one, sum_range_sub, sum_range_sub', sum_range_succ, sum_range_succ', sum_range_succ_comm, sum_range_tsub, sum_sdiff, sum_sdiff_eq_sub, sum_sdiff_eq_sum_sdiff_iff, sum_sdiff_ne_sum_sdiff_iff, sum_sdiff_sub_sum_sdiff, sum_set_coe, sum_singleton, sum_singleton', sum_subset, sum_subset_zero_on_sdiff, sum_subtype, sum_subtype_eq_sum_filter, sum_subtype_map_embedding, sum_subtype_of_mem, sum_sumElim, sum_sum_eq_sum_toLeft_add_sum_toRight, sum_tsub_distrib, sum_union, sum_union_eq_left, sum_union_eq_right, sum_union_inter, sum_unique_nonempty, prod_Prop, prod_fiberwise, prod_fiberwise', prod_of_injective, prod_subset, prod_subsingleton, prod_subtype_mul_prod_subtype, prod_unique, sum_Prop, sum_fiberwise, sum_fiberwise', sum_of_injective, sum_subset, sum_subsingleton, sum_subtype_add_sum_subtype, sum_unique, sum_iff, sum_univ_iff, prod_mul_prod, sum_add_sum, prod_iff, prod_univ_iff, prod_toFinset, sum_toFinset, sum_toFinset_count_eq_length, exists_smul_of_dvd_count, mem_sum, prod_map_prod, prod_sum, sum_count_eq_card, sum_map_sum, sum_sum, toFinset_sum_count_eq, toFinset_sum_count_nsmul_eq, nat_abs_sum_le | 279 |
| Total | 279 |