← all areas

Namespace Polynomial 76 theorems

— 74 · Chebyshev 1 · Monic 1

directly in Polynomial 74

• Polynomial values along t = N^K m are N-adically close to p(0) Polynomial.exists_eval_eq_coeff_zero_add_pow_mul 0 below · cited by 1 · depth 8
• A root of valuation less than one from the Newton polygon Polynomial.exists_isRoot_and_valuation_lt_one 0 below · cited by 1 · depth 8
• Rootless integral specialisations of a weighted polynomial Polynomial.exists_forall_not_isRoot_of_weighted 3 below · cited by 1 · depth 9
• Truncated factorisation at infinity of a weighted polynomial Polynomial.exists_approximants_at_infty 0 below · cited by 1 · depth 10
• Roots of large specialisations lie near a branch Polynomial.exists_branch_near_root 0 below · cited by 1 · depth 10
• Irreducibility from an automorphism cycling all but one root Polynomial.irreducible_of_transitive_ringAut 0 below · cited by 5 · depth 10
• Unique common root of a split separable polynomial is rational Polynomial.mem_range_of_unique_common_root 0 below · cited by 10 · depth 10
• A value attained too often lies in the base field Polynomial.mem_range_of_eval_eq_const 0 below · cited by 1 · depth 12
• Two-chart degree bound on minimal polynomial coefficients Polynomial.natDegree_aeval_symm_minpoly_adjoin_coeff_le_of_transcendental 2 below · cited by 5 · depth 12
• Degree bound from membership in L[x⁻¹] Polynomial.natDegree_le_of_aeval_mul_inv_pow_mem_adjoin_inv 0 below · cited by 1 · depth 13
• Integrality of y⁻¹ from a monic symmetric bivariate relation Polynomial.exists_isIntegral_adjoin_inv_of_bivariate_eq_zero_of_monic_of_symm 0 below · cited by 3 · depth 14
• Simple roots lift under reduction of a split polynomial Polynomial.exists_root_reducing_to_simple_root 0 below · cited by 2 · depth 14
• Many coprime irreducible polynomials mod ℓ of prescribed large degree Polynomial.exists_le_card_lt_monic_irreducible_map_pairwise_isCoprime 0 below · cited by 5 · depth 15
• Coprimality lifts from the residue field for monic f Polynomial.isCoprime_of_monic_of_isCoprime_map_of_maximalIdeal_le_ker 0 below · cited by 3 · depth 15
• Truncated inverse of a polynomial with unit constant term Polynomial.exists_coeff_sum_monomial_mul_sub_one_eq_zero_of_isUnit_coeff_zero 0 below · cited by 2 · depth 16
• Unit value of a polynomial at one of deg D+1 residues Polynomial.exists_isUnit_aeval_of_sub_mem_maximalIdeal_imp_eq 0 below · cited by 2 · depth 16
• Squarefreeness descends along a map from a field into a domain Polynomial.squarefree_of_squarefree_map 0 below · cited by 2 · depth 16
• Kronecker-shape root estimate, quotient form Polynomial.valuation_div_sub_one_lt_one_of_kroneckerShape 1 below · cited by 1 · depth 16
• q-power map commutes with polynomial evaluation over 𝔽_q Polynomial.aeval_pow_card_eq_pow_card 0 below · cited by 1 · depth 17
• The Deuring polynomial has (q-1)/2 distinct roots in characteristic q Polynomial.card_roots_toFinset_deuringPolynomial_map 0 below · cited by 1 · depth 17
• Value at 1 of the Deuring polynomial mod q Polynomial.eval_one_deuringPolynomial_map 0 below · cited by 3 · depth 17
• Functional equation H_q(1-t)=(-1)^m H_q(t) in characteristic q Polynomial.eval_one_sub_deuringPolynomial_map 0 below · cited by 1 · depth 17
• The Deuring polynomial has constant term 1 Polynomial.eval_zero_deuringPolynomial_map 0 below · cited by 4 · depth 17
• Truncated Newton jets with unit derivative Polynomial.exists_coeff_eval_sum_monomial_eq_zero_of_isUnit_derivative 0 below · cited by 1 · depth 17
• Lifting the exponent for Res(Xⁿ-1,P) along ℓ-power multiples Polynomial.exists_factorization_resultant_X_pow_sub_one_eq_mul_add_of_not_dvd 0 below · cited by 1 · depth 17
• Geometric integrality of the rational function field Polynomial.isDomain_tensor_of_isFractionRing 0 below · cited by 1 · depth 17
• Reducedness of D[X]/(g) for g monic and separable over Frac D Polynomial.isReduced_quotient_span_singleton_of_separable_map 0 below · cited by 2 · depth 17
• Coefficient bound by logarithmic Mahler measure Polynomial.log_norm_coeff_le_logMahlerMeasure_add 0 below · cited by 3 · depth 17
• Base change of κ[X]/(f) to D[X]/(f) Polynomial.nonempty_ringEquiv_tensor_quotient_span_singleton 0 below · cited by 1 · depth 17
• Self-reciprocity of the Deuring polynomial Polynomial.pow_mul_eval_inv_deuringPolynomial_map 0 below · cited by 1 · depth 17
• Root-size dichotomy for Kronecker-shaped polynomials over a valued field Polynomial.valuation_root_dichotomy_of_kroneckerShape 0 below · cited by 2 · depth 17
• Irreducibility of Xⁿ - a via a coprime valuation Polynomial.X_pow_sub_C_irreducible_of_isCoprime_apply 0 below · cited by 1 · depth 18
• Finiteness of the critical values of a polynomial Polynomial.finite_setOf_criticalValue 0 below · cited by 1 · depth 18
• Coprimality and non-vanishing Wronskian for composed rational functions Polynomial.isCoprime_and_wronskian_ne_zero_comp_of_wronskian_ne_zero 0 below · cited by 7 · depth 18
• Degree of the Deuring polynomial over any field Polynomial.natDegree_deuringPolynomial_map 0 below · cited by 1 · depth 18
• Exactly one large root of a Kronecker-shape polynomial Polynomial.roots_filter_valuation_eq_singleton_of_kroneckerShape 1 below · cited by 1 · depth 18
• Separability of the Deuring polynomial in characteristic q Polynomial.separable_deuringPolynomial_map 0 below · cited by 2 · depth 18
• Separability of P-c at a non-critical value c Polynomial.separable_sub_C_of_forall_eval_derivative 0 below · cited by 1 · depth 18
• Coefficient bounds for a formal branch through a simple point Polynomial.abv_coeff_mul_pow_le_of_evalEval_C_add_X_eq_zero 1 below · cited by 1 · depth 19
• Uniqueness of roots within μ(g'(a)) (non-archimedean) Polynomial.eq_of_abv_sub_lt_abv_derivative_eval 0 below · cited by 1 · depth 19
• Formal branch through a simple point of a plane curve Polynomial.existsUnique_constantCoeff_eq_and_evalEval_C_add_X_eq_zero 1 below · cited by 1 · depth 19
• Descent of a function through a rational map, up to Frobenius Polynomial.exists_frobenius_iterate_eq_rational_of_comp_rational_eq_rational 0 below · cited by 2 · depth 19
• Non-archimedean proximity of y to the fibre H(X,0)=0 Polynomial.exists_mem_roots_gaussNorm_mul_abv_sub_pow_le_of_evalEval_eq_zero 3 below · cited by 1 · depth 20
• Polynomials are bounded by their Gauss norm on a disc Polynomial.abv_eval_le_gaussNorm 0 below · cited by 1 · depth 21
• Clearing denominators for a ratio of q^s-rational functions Polynomial.exists_eval_mul_cpow_mul_eval_eq_of_ne_zero 0 below · cited by 1 · depth 21
• Nearest root on the non-archimedean closed unit disc Polynomial.exists_mem_roots_gaussNorm_mul_abv_sub_pow_le 1 below · cited by 1 · depth 21
• Monic integer polynomials determined by resultant inequalities Polynomial.eq_of_forall_natAbs_resultant_X_pow_add_C_le 1 below · cited by 1 · depth 22
• Rationality of a torus-weighted double generating series Polynomial.exists_mvPolynomial_forall_hasSum_torusWeight_mul_eq_of_separated_recurrence 0 below · cited by 3 · depth 22
• Non-archimedean Jensen formula on the closed unit disc Polynomial.log_abv_eval_eq_log_gaussNorm_add_sum 0 below · cited by 1 · depth 22
• Monic split polynomials are determined by power sums of roots Polynomial.eq_of_forall_sum_roots_pow_eq 0 below · cited by 5 · depth 23
• Hensel's lemma for coprime monic factorisations Polynomial.exists_monic_mul_eq_and_map_eq_of_isCoprime_of_isAdicComplete 0 below · cited by 4 · depth 23
• Coefficients of maximal valuation count roots in the unit disc Polynomial.coeff_countP_roots_isDominant_of_isAlgClosed 0 below · cited by 2 · depth 24
• Monic rational polynomials determined by resultant inequalities Polynomial.eq_of_forall_abs_resultant_X_pow_add_C_le 1 below · cited by 1 · depth 24
• Multiplicative polynomial functions of monic integer polynomials are resultants Polynomial.exists_monic_eq_resultant_of_mul_of_forall_exists_mvPolynomial 0 below · cited by 1 · depth 24
• Dimension of (X^e-1)-torsion as a sum over divisors Polynomial.finrank_torsionBy_X_pow_sub_one_eq_sum_finrank_torsionBy_cyclotomic 0 below · cited by 1 · depth 24
• Irreducibility of X^N-β via a valuation-like homomorphism Polynomial.irreducible_X_pow_sub_C_of_monoidHom_units_coprime 0 below · cited by 1 · depth 24
• Coprime denominators: z is a polynomial in a transcendental x Polynomial.mem_range_aeval_of_isCoprime_of_pow_mul_eq 0 below · cited by 1 · depth 24
• Cyclotomic torsion dimensions classify ℚ[X]-modules killed by Xⁿ-1 Polynomial.nonempty_linearEquiv_of_finrank_torsionBy_cyclotomic_eq 0 below · cited by 1 · depth 24
• Rationality of torus sums of separated-recurrent double arrays Polynomial.exists_polynomial_forall_tsum_mul_zpow_mul_eval_eq_zpow_mul_eval_of_separatedRational_of_shellRecurrence 2 below · cited by 1 · depth 26
• Recurrent line sums make a double Laurent series rational Polynomial.exists_polynomial_forall_tsum_mul_zpow_eq_of_shellRecurrent_finsum_line 0 below · cited by 2 · depth 27
• Line sums of a separated-rational array satisfy a linear recurrence Polynomial.shellRecurrent_finsum_line_of_separatedRational_of_shellRecurrence 0 below · cited by 1 · depth 27
• Height-one vertical primes avoid polynomials with non-zero reduction Polynomial.aeval_notMem_of_height_eq_one_of_map_residue_ne_zero 0 below · cited by 2 · depth 28
• Absolute irreducibility of F under separable closedness in L Polynomial.irreducible_map_map_algebraicClosure_of_separable_of_forall_isSeparable_mem_range 2 below · cited by 1 · depth 33
• A universal cyclotomic discrete valuation ring over Z₀ Polynomial.exists_isDiscreteValuationRing_algebra_adjoin_eq_top_forall_exists_algHom_map_eq_one_sub_of_sum_range_pow_eq_zero 2 below · cited by 4 · depth 34
• Annihilating polynomial passes to the constant term Polynomial.aeval_eq_zero_of_forall_pos_aeval_sum_pow_smul_eq_zero 0 below · cited by 2 · depth 35
• A quartic functional equation forces P = N² Polynomial.eq_sq_of_mul_comp_neg_X_sub_C_eq_pow_four_of_irreducible 0 below · cited by 1 · depth 35
• Cyclotomic extension with uniformiser 1-ζ_q, all primes q Polynomial.exists_isDiscreteValuationRing_algebra_adjoin_eq_top_forall_exists_algHom_map_eq_one_sub_of_sum_range_pow_eq_zero_of_prime 3 below · cited by 1 · depth 35
• Hensel lifting of a monic coprime factor along a nilpotent thickening Polynomial.existsUnique_monic_map_eq_dvd_of_isCoprime_of_ker_pow_eq_bot 0 below · cited by 2 · depth 37
• Splitting a distinguished monic polynomial over a complete local domain Polynomial.exists_isDomain_isLocalRing_moduleFinite_eq_prod_X_sub_C_of_monic_of_coeff_mem_maximalIdeal 2 below · cited by 1 · depth 37
• Eisenstein polynomials over W₀[[t]] are prime Polynomial.prime_and_isDomain_adjoinRoot_of_monic_of_coeff_mem_maximalIdeal_powerSeries_of_coeff_zero_eq_natCast_mul 4 below · cited by 2 · depth 37
• Monic polynomial with separated roots divides any common vanishing polynomial Polynomial.dvd_of_monic_of_map_eq_prod_X_sub_C_of_forall_eval_eq_zero 0 below · cited by 1 · depth 38
• Rationality forces r=±1 for ℓ-adic linear factors Polynomial.eq_one_or_eq_neg_one_of_map_eq_C_mul_X_add_C_pow 0 below · cited by 1 · depth 38
• Irreducibility of Φ_q over a DVR with uniformiser q Polynomial.irreducible_cyclotomic_fractionRing_of_maximalIdeal_eq_span 0 below · cited by 2 · depth 38
• Rational polynomial with ℓ-adically divisible values is a_g(X+c)^g Polynomial.map_eq_C_mul_X_add_C_pow_of_forall_dvd_eval 0 below · cited by 1 · depth 38

Polynomial.Chebyshev 1

• Completeness of the Chebyshev polynomials Uⱼ on (0,π) Polynomial.Chebyshev.eq_zero_on_Ioo_of_forall_intervalIntegral_mul_U_eq_zero 0 below · cited by 1 · depth 23

Polynomial.Monic 1

• Reduced roots of a monic lift of (a^q-X)(a-X^q) Polynomial.Monic.map_roots_eq_of_map_eq_kroneckerFibre 0 below · cited by 1 · depth 26