Theoremsadd_mem_sup, card_bot, card_le_one_iff_eq_bot, closure_eq_image_sum, closure_eq_mrange, closure_induction_left, closure_induction_right, closure_singleton_eq, closure_singleton_zero, coe_iSup_of_directed, coe_multiples, coe_sSup_of_directedOn, eq_bot_iff_card, eq_bot_of_card_eq, eq_bot_of_card_le, exists_list_of_mem_closure, exists_mem_sup, exists_multiset_of_mem_closure, forall_mem_sup, iSup_induction, iSup_induction', induction_of_closure_eq_top_left, induction_of_closure_eq_top_right, mem_biSup_of_directedOn, mem_closure_pair, mem_closure_singleton, mem_iSup_of_directed, mem_iSup_of_mem, mem_iSup_prop, mem_multiples, mem_multiples_iff, mem_sSup_of_directedOn, mem_sSup_of_mem, mem_sup, mem_sup_left, mem_sup_right, multiples_eq_closure, multiples_le, multiples_zero, sup_eq_range, closure_range_of, mrange_lift, closure_range_of, mrange_lift, coe_powers, of_mclosure_eq_top, addSubmonoidClosure_one, of_mclosure_eq_top, card_bot, card_le_one_iff_eq_bot, closure_eq_image_prod, closure_eq_mrange, closure_induction_left, closure_induction_right, closure_singleton_eq, closure_singleton_one, coe_iSup_of_directed, coe_powers, coe_sSup_of_directedOn, eq_bot_iff_card, eq_bot_of_card_eq, eq_bot_of_card_le, exists_list_of_mem_closure, exists_mem_sup, exists_multiset_of_mem_closure, forall_mem_sup, iSup_induction, iSup_induction', induction_of_closure_eq_top_left, induction_of_closure_eq_top_right, log_mul, log_pow_eq_self, log_pow_int_eq_self, map_powers, mem_biSup_of_directedOn, mem_closure_pair, mem_closure_singleton, mem_closure_singleton_self, mem_iSup_of_directed, mem_iSup_of_mem, mem_iSup_prop, mem_powers, mem_powers_iff, mem_sSup_of_directedOn, mem_sSup_of_mem, mem_sup, mem_sup_left, mem_sup_right, mul_mem_sup, powLogEquiv_apply, powLogEquiv_symm_apply, pow_apply, pow_coe, pow_log_eq_self, pow_right_injective_iff_pow_injective, powers_eq_closure, powers_le, powers_one, sup_eq_range, of_mclosure_eq_top, of_mclosure_eq_top, ofAdd_image_multiples_eq_powers_ofAdd, ofMul_image_powers_eq_multiples_ofMul | 103 |