TheoremsaddFactor_balance, addFactor_deficit_balance_eq_zero, addFactor_submultiset_total_imbalance, addFactor_waste, card_bound, count_deficitMultiset, deficitMultiset_prod_pos, deficit_implies_le_n, ha, hpos, lower_score_1, lower_score_2, lower_score_3, lower_score_3_case1, lower_score_3_case2a, lower_score_3_case2b, lower_score_3_clean, lowest_score, mem_deficitMultiset, replace_balance, replace_div_balance, replace_div_score_le, replace_div_total_imbalance, replace_sum, score_eq, score_le_of_add_submultiset, score_sum_change, score_sum_change_multiset, waste_eq, zero_total_imbalance, L_sub_log_ge_one, balance_inequality_aux, exists_large_prime_of_rough, hL, hL', hL_pos, hM, balance_ge_neg_M_mul_log, balance_large_prime_ge, balance_large_prime_le, balance_medium_prime_ge, balance_medium_prime_le, balance_small_prime_ge, balance_small_prime_le, balance_tiny_prime_ge, bound_score_1, bound_score_2, bound_score_3, bound_score_4, bound_score_5, card, count_bound_aux, count_multiples_le, count_multiples_lower_bound, count_multiples_lower_bound_pow, div_le, factorial_factorization_eq_div, mem_range, score, score_bound, smooth_of_dvd_small_prime, smooth_of_multiple, sum_valuation_eq, sum_valuation_eq_small, sum_valuation_le, sum_valuation_le_M_mul_interval_count, term_bound, valuation_eq_indicator, valuation_eq_one, waste, initial_balance_eq, initial_full_balance_eq, initial_full_balance_ge, initial_full_sum_valuation_eq, initial_full_term_bound, primeCounting_ge_log, rough_qk_prop, rough_set_card_le, rough_set_structure, rough_valuation_eq_k_valuation, rough_valuation_le_log, rough_valuation_sum_le, valuation_eq_one_of_large_prime, Solution_1, Solution_2, exists_phi_div_self_lt, exists_submultiset_prod_between, factorization_prod_eq_count, pairProd_bound, pairProd_length, pairProd_prod, primeCounting_is_o_id, primeCounting_le_bound, prod_one_sub_one_div_prime_tendsto_zero, sum_factorization_eq_sum_multiples, tendsto_primeCounting_div_id_zero | 96 |