Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Added a development of transcendence theory from Daniel J. Bernstein,
currently a verbatim copy of the original: https://cr.yp.to/2024/transcendence-20241221.ml This, among other results, re-proves the transcendence of e (using a different approach from "100/e_is_transcendental.ml") and proves the transcendence of pi: e_is_transcendental = |- ~algebraic_number (cexp (Cx (&1))) pi_is_transcendental = |- ~algebraic_number (Cx pi) as well as the full Lindemann theorem, which easily implies both of those and more: zero_sum_algebraic_exp_algebraic = |- forall S B. FINITE S /\ S SUBSET algebraic_number /\ (forall s. s IN S ==> algebraic_number (B s)) /\ ring_sum complex_ring S (\s. B s * cexp s) = Cx (&0) ==> (forall s. s IN S ==> B s = Cx (&0)) This more general theorem is also commonly known as Hermite-Lindemann or Lindemann-Weierstrass; see the notes near the top of the file for some historical notes and overview of the proofs. New definitions: QinC QinC_ring ZinC ZinC_ring algebraic_number coeff complex_of_int complex_of_num complex_ring complex_root complex_root_powersums const_x_pow distinct_minpolys elementary_sympoly_range expformal functions infinite_geometric_series minimal_polynomial monic monic_vanishing_at monomial_pow monomial_product numpreimages one_minus_constx perm poly_ord poly_pow poly_product poly_reindex poly_sum range ring_hasQ ring_ord ring_squarefree scaled_pow_newton_rightside series_from_coeffs support_le support_le1 support_lt x_derivative x_minus_const x_monomial x_monomial_shift x_poly x_pow x_series x_truncreverse and theorems: COMPLEX_MUL_RINV_UNIQ PID_x_poly_QinC PID_x_poly_field POWSER_MUL_0 QinC_0 QinC_1 QinC_monic_irreducible_complex_roots QinC_over_num QinC_ring_clauses QinC_subring_complex QinC_to_ZinC UFD_x_poly_QinC UFD_x_poly_field ZinC_0 ZinC_1 ZinC_in_QinC ZinC_ring_clauses ZinC_subring_QinC ZinC_subring_complex ZinC_subring_generated_carrier ZinC_subset_QinC add_in_QinC add_in_ZinC algebraic_has_minimal_polynomial algebraic_number_QinC algebraic_number_QinC_explicit algebraic_number_ZinC algebraic_number_ZinC_explicit algebraic_number_add algebraic_number_half algebraic_number_if_monic_vanishing_at algebraic_number_if_monic_vanishing_at_QinC algebraic_number_if_root_irreducible_QinC_poly algebraic_number_ii algebraic_number_is_root_irreducible_QinC_poly algebraic_number_is_root_monic_irreducible_QinC_poly algebraic_number_is_root_unique_monic_irreducible_QinC_poly algebraic_number_is_root_unique_monic_irreducible_QinC_poly_lemma algebraic_number_is_root_unique_monic_irreducible_QinC_poly_simple algebraic_number_mul algebraic_number_neg algebraic_number_root_QinC_poly algebraic_number_root_irreducible_QinC_poly algebraic_number_subring algebraic_number_sum associates_if_mul_unit_const associates_monic_vanishing_at_if_complex associates_monic_vanishing_at_if_complex_lemma bij_finite_ordering binom_coeff binom_reverse_stair_sum binom_rowsum binom_rowsum_partial binom_stair_sum binom_sum botcoeff1_if_x_truncreverse_monic card_empty card_image_permutes card_insert card_le_lt card_o_permutes card_perm card_range carrier_QinC_series_subring_generated_refl coeff_const_x_pow coeff_const_x_pow_times coeff_deg_le coeff_infinite_geometric_series coeff_le_deg coeff_monic_vanishing_at coeff_monic_vanishing_at_lemma coeff_monic_vanishing_at_lemma2 coeff_one_minus_constx coeff_one_minus_constx_times coeff_poly_0 coeff_poly_1 coeff_poly_add coeff_poly_carrier_in_ring coeff_poly_const coeff_poly_const_times coeff_poly_in_ring coeff_poly_mul coeff_poly_mul_lemma coeff_poly_mul_oneindex coeff_poly_neg coeff_poly_sub coeff_poly_subring_if_powersums_subring coeff_poly_subring_if_powersums_subring_lemma coeff_poly_sum coeff_pow_infinite_geometric_series coeff_root_bound_1 coeff_root_bound_mul coeff_root_bound_one_minus_constx coeff_root_bound_pow coeff_root_bound_product coeff_series_add coeff_series_carrier_in_ring coeff_series_from_coeffs coeff_series_in_ring coeff_times_poly_const coeff_x_derivative coeff_x_derivative_poly_mul coeff_x_minus_const coeff_x_minus_const_times coeff_x_pow coeff_x_pow_times coeff_x_truncreverse complex_coeff_x_pow_times complex_field_clauses complex_ring_clauses complex_root_associates complex_root_divides complex_root_if_x_minus_const_divides complex_root_le_deg complex_root_minimal_polynomial_refl complex_root_monic_vanishing_at complex_root_powersums_QinC_monic_irreducible_QinC complex_root_powersums_QinC_monic_irreducible_ZinC complex_root_powersums_ring complex_root_ring complex_root_x_minus_const complex_root_x_pow const_0_x_pow const_1_x_pow const_x_pow_0 const_x_pow_poly const_x_pow_poly_lemma const_x_pow_poly_lemma2 const_x_pow_series coprime_derivative_if_squarefree coprime_poly_if_linear_combination coprime_prime_derivative coprime_product coprimes_sharing_root cproduct_ring_product_complex deg_0_if_unit deg_coeff deg_coeff_from_le deg_const_mul_le deg_const_x_pow deg_const_x_pow_le deg_divides deg_le_coeff deg_monic_poly_mul deg_monic_vanishing_at deg_monic_vanishing_at_le deg_mul_const_const_1 deg_mul_const_le deg_mul_unit_const deg_one_minus_constx_le deg_pow_newton_identities_monic_vanishing_at deg_pow_newton_identities_monic_vanishing_at_lemma deg_prime deg_scaled_pow_newton_rightside deg_x_derivative deg_x_derivative_le deg_x_derivative_lemma deg_x_minus_const deg_x_minus_const_le deg_x_pow deg_x_pow_le deg_x_truncreverse_le deg_zero_ring denominator_if_monic_QinC denominator_reverse denominator_reverse_mul denominator_reverse_pow denominator_reverse_product distinct_minpolys_card_root distinct_minpolys_deg_nonzero distinct_minpolys_denominator distinct_minpolys_distinct_roots distinct_minpolys_finite_root distinct_minpolys_finite_root_simple distinct_minpolys_monic_vanishing_at distinct_minpolys_monic_vanishing_at_simple distinct_minpolys_nonzero distinct_minpolys_reverse_nonzero distinct_minpolys_total_deg distinct_minpolys_zero_root div_in_QinC divides_factor_and_derivative_product divides_le_pow_ring_ord divides_pow_ring_ord e_is_irrational e_is_transcendental elementary_sympoly_range_in_poly_ring elementary_sympoly_range_le elementary_sympoly_range_o_permutes elementary_sympoly_range_subring elim_image_subset_u elim_image_subset_v eq_coeff eval_const_x_pow eval_elementary_sympoly_range eval_elementary_sympoly_range_coeff eval_monic_vanishing_at eval_monic_vanishing_at_refl eval_one_minus_constx eval_poly_pow_multi eval_poly_product eval_poly_product_multi eval_x_minus_const eval_x_minus_const_refl eval_x_pow expformal_0 expformal_linearly_independent expformal_perm_linearly_independent expformal_powersums_QinC extension_z fact_1 fact_binom_lemma_37 fact_binom_lemma_37_real factorial_lower_bound field_QinC field_complex finite_coeff finite_functions finite_le_lt finite_monomial_vars_permutation finite_monomial_vars_permutes finite_monomial_vars_permutes_lemma finite_monomial_vars_swap finite_ordering finite_perm finite_range finite_subsets_card fun_eq_thm_e fun_eq_thm_v functions_empty functions_insert functions_insert_injective functions_to gcd_poly_linear_combination half_not_in_ZinC ii_not_in_ZinC image_card_powerset image_functions_subset image_inverse_permutes image_numpreimages image_numseg_antidiagonal image_o_permutes image_pair image_permutes_arbo_functions image_permutes_arbo_functions_functions image_permutes_o_functions_perm image_permutes_o_perm image_permutes_subset image_surj in_complex_ring in_functions in_image_cd in_image_vw infinite_geometric_series_inverse infinite_geometric_series_powerseries infinite_geometric_series_x_series infinite_monomial_vars_permutes injective_finite_ordering injective_pair_rewrite injective_permutes_arbo_functions injective_permutes_arbo_functions_functions insert_delete_nonmember insert_empty int_in_ZinC int_in_subring int_of_num_sum integral_domain_QinC integral_domain_ZinC integral_domain_complex integral_domain_x_poly_QinC integral_domain_x_poly_field inverse_permutes_o_refl_o irred_x_minus_const is_inters isum_integer_sum lambda_pair_ab lcm_exists lcm_set_exists lcm_set_units le_lt_numseg le_min linear_combination_if_coprime_poly max_finite max_le maybe_algebraic_minimal_polynomial min_le minimal_polynomial_QinC minimal_polynomial_divides minimal_squarefree_from_algebraic_set monic_QinC_squarefree_complex_squarefree monic_QinC_squarefree_complex_squarefree_lemma monic_associates monic_factorization monic_factorization_distinct_minpolys monic_factorization_exponents monic_lcm_set_exists monic_poly_0 monic_poly_1 monic_poly_mul monic_poly_product monic_product_distinct_minpolys monic_squarefree_complex_roots monic_subring monic_vanishing_at_complex_root monic_vanishing_at_empty monic_vanishing_at_eq monic_vanishing_at_if_monic_complex monic_vanishing_at_image monic_vanishing_at_insert monic_vanishing_at_monic monic_vanishing_at_plus1 monic_vanishing_at_poly monic_vanishing_at_series monic_x_minus_const monic_x_pow monic_zero_ring monomial_1_le monomial_1_o_permutes monomial_1_o_permutes_eq monomial_eq_swap monomial_induction monomial_le_mul2_eq monomial_le_swap monomial_pow_0 monomial_pow_1 monomial_pow_add monomial_product_empty monomial_product_insert monomials_poly_reindex mul_expformal mul_in_QinC mul_in_ZinC mul_unit_const_if_associates multi_QinC_to_ZinC multi_monic_factorization_distinct_minpolys neg_in_QinC neg_in_ZinC neg_num_over_num_in_QinC neg_ring_of_num_nonzero newton_identities newton_identities_monic_vanishing_at newton_identities_natural newton_identities_recurrence newton_identities_reverse no_square_divisor_if_coprime_derivative no_square_divisor_if_coprime_derivative_lemma1 no_square_divisor_if_coprime_derivative_lemma2 nonconstant_complex_root nonconstant_complex_x_minus_root nonzero_if_coprime_derivative nonzero_if_x_truncreverse_monic nonzero_one_minus_constx nonzero_poly_mul nonzero_poly_pow nonzero_poly_product nonzero_ring_ord_if_divides not_coprime_QinC_if_shared_complex_root not_squarefree_if_divisible_by_square nsum_delta nsum_reflect_0 num_in_QinC num_in_ZinC num_in_subring num_over_num_in_QinC numpreimages_o_permutes numpreimages_permutes_o_perm numseg_le_lt_reflect numseg_le_reflect_0 o_def_s o_image_permutes o_permutes_cancel o_permutes_subset one_minus_constx_poly one_minus_constx_series ord_minpoly ord_pow_minpoly ord_product_distinct_minpolys ord_product_distinct_minpolys_root ord_product_one_minus_constx_I ord_sum_product_one_minus_constx_I perm_in_permutes perm_set_permutes permutes_o_inverse_refl_o pi_is_transcendental poly_0_QinC_eq_poly_0_complex poly_0_ZinC_eq_poly_0_QinC poly_0_ZinC_eq_poly_0_complex poly_0_o_permutes poly_0_sub poly_0_subring poly_1_0_complex poly_1_QinC_eq_poly_1_complex poly_1_if_monic_deg_0 poly_1_o_permutes poly_1_pow poly_1_subring poly_QinC_if_poly_ZinC poly_add_QinC_eq_poly_add_complex poly_add_in_poly_ring poly_add_o_permutes poly_add_subring poly_coeff poly_complex_if_poly_QinC poly_complex_if_poly_ZinC poly_const_QinC poly_const_QinC_poly_const_complex poly_const_o_permutes poly_const_pow poly_const_product poly_const_subring poly_const_sum poly_const_times poly_deg_pow_le poly_deg_product poly_deg_product_each_le poly_deg_product_le poly_deg_subring poly_deg_sum_le poly_divides_delta poly_divides_product poly_divides_sum poly_eval_expand_coeff poly_eval_subring poly_eval_vsum poly_eval_vsum_lemma poly_evaluate_poly_reindex poly_evaluate_pow poly_evaluate_product poly_evaluate_subring poly_evaluate_sum poly_first_monomial poly_if_coeff poly_in_full_ring poly_lcm_set_exists poly_mul_QinC_eq_poly_mul_complex poly_mul_QinC_poly_mul_complex poly_mul_const_const poly_mul_const_const_1 poly_mul_in_poly_ring poly_mul_o_permutes poly_mul_pow poly_mul_subring poly_mul_sum_mul_delete poly_neg_QinC_eq_poly_neg_complex poly_neg_in_poly_ring poly_neg_o_permutes poly_neg_subring poly_ord_1 poly_ord_add_dominant poly_ord_add_ge poly_ord_const poly_ord_derivative_ge poly_ord_derivative_pole poly_ord_derivative_pole_lemma poly_ord_exists poly_ord_exists_lemma poly_ord_exists_lemma2 poly_ord_ge poly_ord_ge_if poly_ord_monic_vanishing_at poly_ord_monic_vanishing_at_numpreimages poly_ord_mul poly_ord_mul_0 poly_ord_mul_ge0_ge poly_ord_mul_ge_ge poly_ord_mul_ge_ge0 poly_ord_neg_ge poly_ord_one_minus_constx poly_ord_pow poly_ord_product poly_ord_sub_dominant poly_ord_sub_ge poly_ord_sum_dominant poly_ord_sum_ge poly_ord_unique poly_ord_unique_0 poly_ord_unique_1 poly_ord_x_minus_const poly_ord_x_pow poly_ord_x_pow_1 poly_pow_0 poly_pow_1 poly_pow_add poly_pow_in_poly_ring poly_pow_is_product poly_pow_mul poly_pow_newton_identities_monic_vanishing_at poly_pow_newton_identities_monic_vanishing_at_lemma poly_pow_o_permutes poly_pow_poly poly_pow_series poly_pow_subring poly_product_1 poly_product_botcoeff1 poly_product_const poly_product_delete poly_product_empty poly_product_eq poly_product_image poly_product_in_poly_ring poly_product_insert poly_product_o_permutes poly_product_poly poly_product_poly_multi poly_product_pow poly_product_restrict_subset poly_product_ring_product_x_poly poly_product_series poly_product_series_multi poly_product_subring poly_product_subring_multi poly_reindex_permutes poly_reindex_subring poly_ring_carrier poly_ring_use_pow poly_scaled_pow_newton_rightside poly_series_from_coeffs poly_sub_0 poly_sub_in_poly_ring poly_sub_ldistrib poly_sub_ldistrib_lemma poly_sub_o_permutes poly_sub_rdistrib poly_sub_rdistrib_lemma poly_sub_subring poly_subring_if_powersums_subring poly_sum_const poly_sum_delete2 poly_sum_empty poly_sum_eq poly_sum_insert poly_sum_lmul poly_sum_poly poly_sum_poly_multi poly_sum_restrict_subset poly_sum_ring_sum_x_poly poly_sum_series poly_sum_subring_multi poly_use poly_var_o_permutes poly_var_subring poly_vars_empty poly_vars_poly_reindex poly_vars_pow poly_vars_pow_subset poly_vars_product_poly_subset poly_vars_subring poly_vars_sum_poly_subset polynomial_elementary_sympoly_range polynomial_if_coeff polynomial_o_permutes polynomial_poly_reindex polynomial_product_distinct_minpolys pow_expformal pow_expformal_powersums_QinC pow_infinite_geometric_series pow_infinite_geometric_series_inverse pow_infinite_geometric_series_inverse_lemma pow_newton_identities_monic_vanishing_at pow_newton_identities_natural powerseries_elementary_sympoly_range powerseries_o_permutes powerseries_poly_reindex powerset_insert_disjoint powersums_subring_if_poly_subring powersums_subring_if_poly_subring_denominators powersums_subring_if_poly_subring_denominators_waterfall powser_product_o_permutes powser_ring_carrier powser_use prime_divides_prime_and prime_if_deg_1 prime_iff_irreducible_over_field primefact_divides primefact_ord primefact_ord_waterfall prod_resolvent_if_poly_QinC prod_resolvent_if_poly_QinC_lemma product_coprime_primes_divides product_coprime_primes_divides_waterfall product_expformal product_expformal_I product_functions_sum_mul_cexp_expand product_functions_sum_mul_expformal_expand product_perm_sum_mul_cexp_expand product_perm_sum_mul_expformal_expand product_perm_sum_mul_expformal_expand_v2 product_perm_sum_mul_expformal_expand_v3 product_times_sum_reciprocals properly_le range_0 range_add_1_delete_refl range_lt range_set_lt real_of_num_plus_minus_minus resolvent_if_poly_QinC resolvent_if_powersums_QinC ring_1_0_QinC ring_1_0_complex ring_add_sub_cancel ring_associates_ord ring_char_QinC ring_char_ZinC ring_char_complex ring_char_x_series ring_coprime_1 ring_coprime_associates_prime ring_coprime_if_unit ring_coprime_lpow ring_coprime_lrpow ring_coprime_product ring_coprime_product_waterfall ring_coprime_rpow ring_div_complex ring_div_refl ring_divides_associates_prime ring_divides_poly_complex_if_ring_divides_poly_QinC ring_divides_pow_pow ring_divides_product ring_exp_sum ring_hasQ_QinC ring_hasQ_neg ring_hasQ_subring_series_complex ring_inv_complex ring_mul_sum_mul_delete ring_of_int_complex ring_of_num_QinC ring_of_num_ZinC ring_of_num_complex ring_of_num_injective ring_of_num_injective_lemma ring_of_num_nonzero ring_of_num_x_series ring_ord_1 ring_ord_associates ring_ord_associates_eq ring_ord_divides ring_ord_divides_eq ring_ord_exists ring_ord_exists_unique ring_ord_gcd ring_ord_lcm ring_ord_lcm_set ring_ord_mul ring_ord_notdivides ring_ord_pow ring_ord_pow_refl ring_ord_prime ring_ord_prime_divides ring_ord_product ring_ord_product_waterfall ring_ord_refl ring_ord_squarefree ring_ord_unique ring_ord_unique_lemma ring_ord_unit ring_polynomial_if_subring ring_polynomial_subring_if_coeffs ring_polynomial_subring_product ring_polynomial_subring_sum ring_polynomial_subring_var ring_pow_QinC ring_pow_ZinC ring_pow_complex ring_pow_in_subring ring_pow_is_product ring_pow_neg_1_mul_refl ring_pow_neg_1_plus1 ring_pow_product ring_pow_sub1 ring_powerseries_if_polynomial ring_powerseries_subring ring_prime_divides_lcm_set ring_product_1_plus_expand ring_product_collect ring_product_const ring_product_delete ring_product_delta_delta ring_product_divides_factor_by_factor ring_product_divides_if_coprime ring_product_divides_if_coprime_waterfall ring_product_eq_0 ring_product_fiber_o ring_product_functions_sum_mul_exp_expand ring_product_in_subring ring_product_o ring_product_o_v2 ring_product_perm_sum_mul_exp_expand ring_product_poly_o_permutes ring_product_poly_o_permutes_waterfall ring_product_subring_generated ring_product_subring_generated_v2 ring_product_sum_expand ring_squarefree_associates ring_squarefree_if_prime ring_squarefree_if_product_coprime_primes ring_squarefree_if_product_coprime_primes_indexed ring_squarefree_if_unit ring_squarefree_lcm ring_squarefree_lcm_set ring_sub_QinC ring_sub_complex ring_sum_1 ring_sum_const ring_sum_cross_mul ring_sum_delete2 ring_sum_delta_delta ring_sum_eq_name_d ring_sum_fiber_o ring_sum_image_injective ring_sum_image_injective_pair ring_sum_image_x_monomial ring_sum_image_x_monomial_pair ring_sum_in_subring ring_sum_insert_top ring_sum_num ring_sum_numseg_0_diff ring_sum_numseg_0_diff_reflect ring_sum_numseg_le_expand ring_sum_numseg_le_offset ring_sum_numseg_le_reflect ring_sum_o ring_sum_o_v2 ring_sum_o_v3 ring_sum_poly_o_permutes ring_sum_range_add_1 ring_sum_range_add_1_sub ring_sum_restrict_subset ring_sum_shift1 ring_sum_sub ring_sum_subring_generated ring_sum_subring_generated_v2 scaled_pow_newton_identities_monic_vanishing_at scaled_pow_newton_identities_monic_vanishing_at_lemma select_foreach series_QinC_if_series_ZinC series_complex series_complex_if_series_QinC series_from_coeffs_coeff series_in_full_ring series_series_from_coeffs series_sum_series_multi square_divides_if_also_divides_derivative square_divides_product_if_factor_divides_factor squarefree_from_algebraic_set squarefree_from_algebraic_set_avoiding_0 squarefree_if_coprime_derivative squarefree_if_irreducible_over_field sub_in_subring subring_QinC_empty subring_QinC_empty_lemma subring_complex_QinC subring_complex_QinC_lemma subring_complex_ZinC subring_complex_ZinC_lemma subring_complex_empty subring_complex_empty_lemma subring_const_x_pow subring_x_pow subset_full_card subset_y subsets_card_0 subsets_card_toobig subsets_full_card subsets_full_card_empty sum_QinC_eq_sum_complex sum_real_of_int sum_root_decomposition_if_monic_vanishing_at_factorization sum_root_decomposition_if_monic_vanishing_at_factorization_lemma support_le1_elementary_sympoly_range support_le1_mul support_le1_poly_1 support_le1_pow support_le1_pow_elementary_sympoly_range support_le1_product support_le1_product_pow_elementary_sympoly_range support_le1_product_pow_elementary_sympoly_range_v2 support_le_0 support_le_cancel support_le_elementary_sympoly_range support_le_exists support_le_mul support_le_mul_top support_le_poly_1 surjective_finite swap_permutes_range symfun_expformal_powersums_QinC symfun_expformal_powersums_QinC_v2 symfun_expformal_powersums_QinC_v3 symfun_subring_if_powersums_subring symmetric_subring_if_poly_subring symmetric_subring_if_poly_subring_lemma symmetric_subring_if_poly_subring_range term_le_nsum topcoeff_monic_poly_mul topcoeff_monic_vanishing_at topcoeff_nonzero transcendence_A_nonnegative transcendence_Gp_poly transcendence_H_botcoeff1 transcendence_H_bound transcendence_H_deg_G transcendence_H_deg_G_lemma transcendence_H_deg_HG transcendence_H_deg_HG_simpler transcendence_H_deg_overall transcendence_H_denom transcendence_H_main transcendence_H_poly transcendence_H_pow_denom transcendence_H_product transcendence_H_product_complex_ring transcendence_Hk_bound transcendence_Htimes_poly transcendence_Huv_lemma transcendence_Hv_bound transcendence_Hv_denom transcendence_Hv_induction transcendence_Hv_kexists transcendence_Hv_kexists_v2 transcendence_Hv_noupperbound transcendence_Hv_poly transcendence_Hv_zero transcendence_Hv_zero_Ptrivial transcendence_Hv_zero_k0 transcendence_Hw_denom transcendence_all_0 transcendence_all_0_QinC transcendence_all_0_QinC_monic_vanishing_at transcendence_all_0_QinC_weight1 transcendence_all_0_ZinC transcendence_mostly_0 transcendence_mostly_0_x transcendence_newton_He_Ge transcendence_newton_Hk transcendence_newton_Hk_psum transcendence_newton_pe transcendence_ord_H transcendence_ord_Hk transcendence_ord_Hku transcendence_ord_Hu transcendence_ord_revp transcendence_p_bound transcendence_pole_order_ne1 transcendence_u_tail transcendence_uv_diffeq transcendence_uv_trivial transcendence_v_bound transcendence_v_denom transcendence_vw_diff transcendence_vw_diff_series transcendence_vw_diff_series_H transcendence_vw_match transcendence_w_denom transcendence_weighted_QinC_monic_vanishing_at transcendental_if_exp_nonzero_algebraic unique_prime_valuation unique_prime_valuation_lemma vandermonde_indep vandermonde_indep_range vsum_delta_complex vsum_ring_sum_complex weighted_powersums_distinct_minpolys x_derivative_add_series x_derivative_const_x_pow x_derivative_monic_vanishing_at x_derivative_mul x_derivative_mul_const x_derivative_neg_series x_derivative_nonzero x_derivative_one_minus_constx x_derivative_poly_0 x_derivative_poly_1 x_derivative_poly_const x_derivative_poly_const_mul_series x_derivative_polynomial x_derivative_pow x_derivative_product x_derivative_ratio_scaling x_derivative_series x_derivative_sub_series x_derivative_subring x_derivative_sum x_derivative_x_minus_const x_derivative_x_pow x_minus_const_0 x_minus_const_QinC_eq_x_minus_const_complex x_minus_const_nonzero x_minus_const_not_unit x_minus_const_poly x_minus_const_series x_monomial_0_monomial_1 x_monomial_add x_monomial_deg x_monomial_factorizations x_monomial_factorizations_set x_monomial_injective x_monomial_mul_shift x_monomial_pair_injective x_monomial_shift_eq_x_monomial x_monomial_shift_injective x_monomial_shift_is_not_monomial_1 x_monomial_shift_mul x_monomial_surjective x_poly_QinC_is_ZinC_denominator x_poly_QinC_is_ZinC_denominator_v2 x_poly_QinC_is_ZinC_denominator_v2_lemma x_poly_QinC_is_ZinC_denominator_v2_lemma2 x_poly_ZinC_denominator_is_QinC x_poly_ZinC_denominator_is_QinC_v2 x_poly_ZinC_denominator_is_QinC_v2_lemma x_poly_ZinC_denominator_is_QinC_v2_lemma2 x_poly_carrier x_poly_carrier_in_series_carrier x_poly_carrier_subset_series_carrier x_poly_field_monic_associate x_poly_mul_in_QinC_eq_0 x_poly_sub_use x_poly_subring_in_poly_carrier x_poly_use x_poly_use_pow x_poly_vars_1 x_pow_0 x_pow_1 x_pow_QinC_eq_x_pow_complex x_pow_add x_pow_poly x_pow_pow x_pow_series x_series_carrier x_series_monomial_mul_finite x_series_sub_use x_series_use x_series_use_pow x_truncreverse_0_poly_const x_truncreverse_const_x_pow x_truncreverse_derivative_monic_vanishing_at x_truncreverse_monic_vanishing_at x_truncreverse_mul x_truncreverse_one_minus_constx x_truncreverse_poly x_truncreverse_poly_0 x_truncreverse_poly_1 x_truncreverse_poly_add x_truncreverse_poly_const x_truncreverse_poly_sub x_truncreverse_poly_sum x_truncreverse_pow x_truncreverse_product x_truncreverse_series x_truncreverse_subring x_truncreverse_x_minus_const x_truncreverse_x_pow zero_if_ZinC_norm_lt1 zero_if_ZinC_scale_bound zero_lcm zero_lcm_set zero_sum_QinC_exp_algebraic zero_sum_QinC_exp_squarefree_roots zero_sum_QinC_exp_squarefree_roots_lemma_denouement zero_sum_QinC_exp_squarefree_roots_lemma_sym_coeff_poly zero_sum_QinC_exp_squarefree_roots_lemma_sym_poly zero_sum_QinC_exp_squarefree_roots_lemma_sym_powersums zero_sum_algebraic_exp_algebraic zero_sum_nonzero_algebraic_exp_algebraic zero_sum_nonzero_algebraic_exp_algebraic_lemma_sym
- Loading branch information
