| Name | Category | Theorems |
|---|
degree π | CompOp | 278 mathmath: degree_map_le, degree_normalize, modByMonic_eq_self_iff, IsAlgClosed.roots_eq_zero_iff_degree_nonpos, WittVector.RecursionMain.succNthDefiningPoly_degree, degree_mul_le, exists_degree_le_of_mem_span_of_finite, degree_scaleRoots, coe_lt_degree, degree_le_degree, degree_smul_of_smul_regular, MonicDegreeEq.degree, lifts_and_degree_eq_and_monic, Lagrange.degree_basisDivisor_self, Cubic.degree_of_b_eq_zero, degree_quadratic_lt, degree_pow_le, zero_le_degree_iff, Sequence.degree_eq', degree_pow, mod_eq_self_iff, PowerSeries.degree_weierstrassMod_lt, degree_eq_natDegree, degree_gcd_le_left, degree_C_mul_of_isUnit, degree_mul_leadingCoeff_inv, length_coeffList_eq_withBotSucc_degree, degree_le_of_dvd, div_tendsto_zero_iff_degree_lt, integralNormalization_degree, degree_list_prod, degree_lt_degree_mul_X, Splits.degree_le_one_of_irreducible, divByMonic_eq_zero_iff, minpoly.degree_pos, degree_C_mul_of_mul_ne_zero, tendsto_atTop_iff_leadingCoeff_nonneg, IsDistinguishedAt.degree_eq_coe_lift_order_map, degree_list_prod_le, Lagrange.eq_interpolate_iff, int_coeff_of_cyclotomic', degree_X_pow_add_C, degree_pos_of_root, degree_X_sub_C, PowerSeries.degree_trunc_lt, card_roots_map_le_degree, Cubic.degree_of_a_eq_zero', MvPolynomial.degree_optionEquivLeft, degree_map_eq_of_isUnit_leadingCoeff, degree_restriction, degree_mono, Splits.degree_eq_card_roots, degree_C_lt_degree_C_mul_X, tendsto_atBot_iff_leadingCoeff_nonpos, Cubic.degree_of_a_ne_zero', degree_quadratic, minpoly.degree_le, abs_tendsto_atTop_iff, degree_eq_degree_of_associated, PowerSeries.IsWeierstrassDivisionAt.degree_lt, degree_lt_wf, degree_cubic_lt, degree_C, degree_modByMonic_le, Splits.degree_eq_one_of_irreducible, natDegree_lt_natDegree_iff, Matrix.charpoly_degree_eq_dim, int_cyclotomic_rw, coeffList_eraseLead, degree_divX_lt, degree_eraseLead_lt, Chebyshev.degree_T, degree_X_pow_le, degree_monomial_le, natDegree_lt_iff_degree_lt, Lagrange.degree_interpolate_erase_lt, degree_quadratic_le, Lagrange.degree_interpolate_lt, abs_tendsto_atBot_iff, degree_X_le, Sequence.degree_eq, Cubic.degree_of_d_ne_zero, degree_derivative_lt, minpoly.degree_le_of_ne_zero, div_eq_quo_add_sum_rem_div, degree_freeMonic, PowerBasis.mem_span_pow', WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis, degree_derivative_eq, degree_erase_lt, degree_le_of_natDegree_le, Splits.def, Lagrange.degree_basisDivisor_of_ne, degree_taylor, PowerBasis.degree_minpoly, degree_map_eq_of_leadingCoeff_ne_zero, splits_iff, degree_sum_le, degree_pos_of_ne_zero_of_nonunit, degree_hermite, Irreducible.degree_pos, Lagrange.degree_nodal, Monic.degree_pos, degree_multiset_prod_of_monic, Cubic.degree_of_d_eq_zero, degree_integralNormalization, degree_X_pow_sub_C, degree_le_natDegree, degree_mul_leadingCoeff_self_inv, degree_divByMonic_le, degree_le_mul_left, exists_multiset_roots, Ideal.mem_leadingCoeffNth, degree_C_lt, degree_C_mul_X_pow_le, degree_zero, rootOfSplits'_eq_rootOfSplits, degree_intCast_le, div_eq_zero_iff, exists_degree_le_of_mem_span, Chebyshev.degree_U_of_ne_neg_one, eraseLead_degree_le, degree_X_sub_C_le, degree_eq_iff_natDegree_eq_of_pos, degree_C_mul_X_le, degree_wronskian_lt_add, degree_map_eq_of_injective, degree_mul', degree_one_le, tendsto_nhds_iff, Chebyshev.degree_U_neg_one, degree_cubic, Cubic.degree_of_a_eq_zero, degree_smul_of_isRightRegular_leadingCoeff, monomial_mem_lifts_and_degree_eq, degree_X_pow, Cubic.equiv_symm_apply_b, Lagrange.degree_basis, degree_one, Splits.splits, minpoly.IsIntegrallyClosed.degree_le_of_ne_zero, degree_prod_le, div_eq_quo_add_rem_div, degree_prod, degree_zero_le, Monic.degree_pos_of_not_isUnit, isBoundedUnder_abs_atBot_iff, WeierstrassCurve.Affine.degree_polynomial, degree_pos_of_not_isUnit_of_dvd_monic, LinearRecurrence.charPoly_degree_eq_order, Lagrange.degree_interpolate_le, Cubic.degree_of_c_ne_zero, Cubic.degree_of_a_ne_zero, minpoly.min, MvPolynomial.degree_finSuccEquiv, mem_closure_X_union_C, supDegree_eq_degree, Field.primitive_element_iff_minpoly_degree_eq, degree_X, degree_multiset_prod_le, degree_prod_of_monic, degree_sub_le, degree_of_subsingleton, Monic.degree_mul, Matrix.charpoly_sub_diagonal_degree_lt, degree_eq_zero_of_isUnit, degree_smul_le, Cubic.equiv_symm_apply_c, minpoly.degree_eq_one_iff, degree_lt_degree, degree_C_mul, degree_neg, degree_le_iff_coeff_zero, isBoundedUnder_abs_atTop_iff, card_roots, ofFn_degree_lt, IsSepClosed.degree_eq_one_of_irreducible, degree_eq_card_roots, degree_add_degree_leadingCoeff_inv, PowerBasis.degree_minpolyGen, degree_modByMonic_lt, Cubic.degree_of_d_eq_zero', degree_eq_one_of_irreducible_of_splits, degree_lt_iff_coeff_zero, degree_map_eq_iff, mem_lifts_and_degree_eq, div_tendsto_atBot_zero_iff_degree_lt, degree_comp_neg_X, div_eq_quo_add_rem_div_add_rem_div, degree_le_zero_iff, degree_toSubring, degree_add_le, isUnit_iff_degree_eq_zero, degree_pos_of_aeval_root, degree_cyclotomic', le_degree_of_ne_zero, Cubic.equiv_apply_coe, PowerSeries.IsWeierstrassFactorization.degree_eq_coe_lift_order_map, degree_eq_one_of_irreducible_of_root, degree_mul_X, le_degree_of_mem_supp, degree_annIdealGenerator_le_of_mem, degree_mul_C_of_isUnit, PowerSeries.IsWeierstrassFactorizationAt.degree_eq_coe_lift_order_map_of_ne_top, abs_isBoundedUnder_iff, natDegree_eq_zero_iff_degree_le_zero, PowerSeries.isWeierstrassDivisionAt_iff, degree_update_le, integralNormalization_coeff, Cubic.degree_of_b_ne_zero', degree_leadingCoeff_inv, Sequence.degree_strictMono, degree_shiftedLegendre, degree_pos_of_irreducible, Cubic.degree_of_b_eq_zero', degree_map, degree_cubic_le, Cubic.degree_of_c_ne_zero', Cubic.degree_of_d_ne_zero', Cubic.equiv_symm_apply_d, degree_div_le, Irreducible.degree_le_two, degree_linear_le, degree_eq_card_roots', degree_linear_lt_degree_C_mul_X_sq, degree_cyclotomic_pos, degree_pos_of_evalβ_root, withBotSucc_degree_eq_natDegree_add_one, degree_quadratic_lt_degree_C_mul_X_cb, Cubic.degree_of_c_eq_zero, Cubic.equiv_symm_apply_a, degree_C_mul_X, degree_pow', degree_mul_C, natDegree_pos_iff_degree_pos, degree_mod_lt, degree_multiset_prod, mem_degreeLE, splits_iff_splits, degree_sum_fin_lt, IsAlgClosed.degree_eq_one_of_irreducible, degree_eq_iff_natDegree_eq, degree_map_lt, Cubic.degree_of_c_eq_zero', natDegree_le_iff_degree_le, Sequence.basis_degree_strictMono, degree_add_eq_of_leadingCoeff_add_ne_zero, degree_monomial, degree_mul_X_pow, div_tendsto_atTop_zero_iff_degree_lt, degree_C_mul_X_pow, Monic.degree_map, Monic.degree_mul_comm, Chebyshev.degree_U_natCast, degree_erase_le, degree_cyclotomic, leadingCoeff_eq_zero_iff_deg_eq_bot, Cubic.degree_of_zero, degree_derivative_le, degree_linear, mem_degreeLT, Monic.degree_le_zero_iff_eq_one, PowerBasis.dim_le_degree_of_root, degree_eq_bot, degree_list_sum_le, degree_linear_lt, degree_natCast_le, degree_coe_units, degree_modByMonic_le_left, exists_mul_add_mul_eq_C_resultant, Cubic.degree_of_b_ne_zero, roots_def, degree_X_add_C, degree_radical_le, degree_mul, degree_gcd_le_right, degree_C_le, int_cyclotomic_spec
|
leadingCoeff π | CompOp | 216 mathmath: natDegree_mul_leadingCoeff_inv, leadingCoeff_mul_X_pow, eq_X_sub_C_of_separable_of_root_eq, coe_normUnit_of_ne_zero, splits_iff_exists_multiset, RatFunc.num_div, isEquivalent_atBot_div, AdjoinRoot.minpoly_root, norm_leadingCoeff_eq_one_of_mahlerMeasure_eq_one, leadingCoeff_multiset_prod', mahlerMeasure_eq_leadingCoeff_mul_prod_roots, coeffList_eq_cons_leadingCoeff, div_def, div_tendsto_atTop_leadingCoeff_div_of_degree_eq, leadingCoeff_map', Monic.leadingCoeff_C_mul, leadingCoeff_quadratic, leadingCoeff_dvd_leadingCoeff, leadingCoeff_C_mul_of_isUnit, div_tendsto_atBot_leadingCoeff_div_of_degree_eq, leadingCoeff_one, Lagrange.leadingCoeff_basis, leadingCoeff_det_X_one_add_C, mirror_trailingCoeff, Splits.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff, WeierstrassCurve.leadingCoeff_preΞ¨', minpoly.eq_of_irreducible, Splits.eval_derivative, degree_mul_leadingCoeff_inv, eq_prod_roots_of_splits, leadingCoeff_opRingEquiv, eraseLead_add_C_mul_X_pow, coeff_natDegree, coeff_taylor_natDegree, leadingCoeff_mul, WeierstrassCurve.leadingCoeff_preΞ¨β, leadingCoeff_X_pow_add_C, leadingCoeff_hermite, self_sub_monomial_natDegree_leadingCoeff, tendsto_atTop_iff_leadingCoeff_nonneg, isEquivalent_atTop_lead, integralNormalization_aeval_eq_zero, leadingCoeff_zero, reverse_trailingCoeff, leadingCoeff_smul_integralNormalization, Chebyshev.leadingCoeff_U_natCast, exists_finset_of_splits, leadingCoeff_cons_eraseLead, irreducible_mul_leadingCoeff_inv, leadingCoeff_cubic, leadingCoeffHom_apply, eval_derivative_of_splits, tendsto_atBot_iff_leadingCoeff_nonpos, leadingCoeff_mul_prod_normalizedFactors, leadingCoeff_linear, natDegree_mul_leadingCoeff_self_inv, leadingCoeff_normalize, WeierstrassCurve.leadingCoeff_Ξ¨βSq, coeff_zero_eq_leadingCoeff_mul_prod_roots_of_splits, resultant_eq_prod_eval, minpoly.IsIntegrallyClosed.isIntegral_iff_leadingCoeff_dvd, RatFunc.numDenom_div, coeffList_eraseLead, head_coeffList, Cubic.leadingCoeff_of_b_ne_zero', resultant_dvd_leadingCoeff_pow, exists_isIntegral_leadingCoeff_pow_smul_sub_of_isIntegralElem_of_mul_mem_range, leadingCoeff_pow_X_add_C, Chebyshev.leadingCoeff_le_of_forall_abs_le_one, leadingCoeff_X_pow_sub_C, Splits.eq_prod_roots, div_wf_lemma, eq_X_add_C_of_degree_eq_one, WeierstrassCurve.leadingCoeff_preΞ¨, coeff_pow_mul_natDegree, Splits.aeval_eq_prod_aroots, Splits.eq_X_sub_C_of_single_root, Ideal.mem_leadingCoeff, Lagrange.leadingCoeff_eq_sum, logMahlerMeasure_eq_log_leadingCoeff_add_sum_log_roots, mirror_leadingCoeff, integralNormalization_evalβ_eq_zero, IsUnitTrinomial.leadingCoeff_isUnit, leadingCoeff_add_of_degree_eq, content_mul_aux, leadingCoeff_X, degree_mul_leadingCoeff_self_inv, leadingCoeff_prod, Ideal.mem_leadingCoeffNth, isEquivalent_atTop_div, RingHom.isIntegralElem_leadingCoeff_mul, leadingCoeff_pow', comp_neg_X_leadingCoeff_eq, Cubic.leadingCoeff_of_c_eq_zero', eq_prod_roots_of_splits_id, eraseLead_add_monomial_natDegree_leadingCoeff, eval_eq_prod_roots_sub_of_splits_id, Cubic.leadingCoeff_of_a_ne_zero, isEquivalent_atBot_lead, leadingCoeff_mul_X, den_dvd_of_is_root, dvd_mul_leadingCoeff_inv, C_mul_X_pow_eq_self, leadingCoeff_X_pow, sylvesterDeriv_updateRow, leadingCoeff_sum_of_degree_eq, div_tendsto_leadingCoeff_div_of_degree_eq, leadingCoeff_smul_of_smul_regular, Monic.leadingCoeff_notMem, Splits.eval_eq_prod_roots, leadingCoeff_sub_of_degree_lt, tendsto_nhds_iff, leadingCoeff_C_mul_X_pow, int_leadingCoeff_eq, coeff_scaleRoots_natDegree, leadingCoeff_comp, isEisensteinAt_iff, leadingCoeff_map_of_injective, RatFunc.denom_div, leadingCoeff_divByMonic_of_monic, leadingCoeff_preHilbertPoly, aeval_derivative_of_splits, WeierstrassCurve.leadingCoeff_Ξ¦, leadingCoeff_monic_mul, leadingCoeff_mul_C_of_isUnit, WeierstrassCurve.leadingCoeff_Ξ¨Sq, eq_mul_leadingCoeff_of_monic_of_dvd_of_natDegree_le, leadingCoeff_C_mul_X, C_leadingCoeff_mul_prod_multiset_X_sub_C, leadingCoeff_sub_of_degree_eq, trinomial_leadingCoeff, IsIntegrallyClosed.eq_map_mul_C_of_dvd, monic_mul_leadingCoeff_inv, eq_X_sub_C_of_splits_of_single_root, leadingCoeff_mul', leadingCoeff_expand, leadingCoeff_X_sub_C, head?_coeffList, RatFunc.num_div_dvd', aeval_eq_prod_aroots_sub_of_splits, integralNormalization_coeff_mul_leadingCoeff_pow, leadingCoeff_add_of_degree_lt, degree_add_degree_leadingCoeff_inv, leading_coeff_le_mahlerMeasure, Algebra.exists_aeval_invOf_eq_zero_of_idealMap_adjoin_sup_span_eq_top, coe_normUnit, leadingCoeff_eraseLead_eq_nextCoeff, resultant_deriv, exists_leadingCoeff_pow_smul_mem_conductor, integralNormalization_coeff_degree_ne, Splits.coeff_zero_eq_leadingCoeff_mul_prod_roots, integralNormalization_mul_C_leadingCoeff, leadingCoeff_map_of_leadingCoeff_ne_zero, leadingCoeff_mul_monic, fwdDiff_iter_degree_eq_factorial, hasseDeriv_natDegree_eq_C, AdjoinRoot.minpoly_powerBasis_gen, Monic.isUnit_leadingCoeff_of_dvd, evalβ_derivative_of_splits, coeff_eq_esymm_roots_of_card, leadingCoeff_multiset_prod, Cubic.leadingCoeff_of_c_eq_zero, Monic.def, leadingCoeff_X_pow_sub_one, minpoly.IsIntegrallyClosed.isIntegral_iff_isUnit_leadingCoeff, integralNormalization_coeff, degree_leadingCoeff_inv, coeff_eq_esymm_roots_of_splits, reverse_leadingCoeff, leadingCoeff_scaleRoots, leadingCoeff_div, leadingCoeff_C, signVariations_eq_eraseLead_add_ite, leadingCoeff_map, leadingCoeff_X_pow_add_one, leadingCoeff_pow, leadingCoeff_sub_of_degree_lt', scaleRoots_zero, Chebyshev.leadingCoeff_T, splits_iff_exists_multiset', Monic.leadingCoeff, Cubic.leadingCoeff_of_c_ne_zero, splits_of_exists_multiset, leadingCoeff_of_injective, leadingCoeff_monomial, coeff_zero_reverse, Cubic.leadingCoeff_of_b_ne_zero, content_eq_gcd_leadingCoeff_content_eraseLead, monomial_natDegree_leadingCoeff_eq_self, leadingCoeff_prod', leadingCoeff_X_add_C, Cubic.leadingCoeff_of_a_ne_zero', eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le, Cubic.leadingCoeff_of_c_ne_zero', integralNormalization_coeff_ne_natDegree, coeff_comp_degree_mul_degree, leadingCoeff_eq_zero, IsEisensteinAt.leading, mod_def, leadingCoeff_divByMonic_X_sub_C, isIntegral_leadingCoeff_smul, coeff_mul_degree_add_degree, leadingCoeff_eq_zero_iff_deg_eq_bot, Chebyshev.leadingCoeff_eq_iff_of_forall_abs_le_one, leadingCoeff_neg, Module.End.eigenspace_aeval_polynomial_degree_1, IsMonicOfDegree.leadingCoeff_eq, self_sub_C_mul_X_pow, resultant_integralNormalization, WeierstrassCurve.leadingCoeff_Ξ¨β, abs_leadingCoeff_eq_one_of_mahlerMeasure_eq_one, leadingCoeff_add_of_degree_lt', integralNormalization_evalβ_leadingCoeff_mul, leadingCoeff_taylor, nextCoeff_eq_neg_sum_roots_mul_leadingCoeff_of_splits, isIntegral_isLocalization_polynomial_quotient
|
natDegree π | CompOp | 494 mathmath: natDegree_mul_X_pow, natDegree_mul_leadingCoeff_inv, natDegree_hermite, natSepDegree_le_natDegree, natDegree_pos_of_monic_of_aeval_eq_zero, Irreducible.natDegree_le_two, IsPurelyInseparable.minpoly_natDegree_eq', PowerBasis.exists_eq_aeval, NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply, Sequence.basis_natDegree_strictMono, IntermediateField.adjoin.finrank, natDegree_le_iff_coeff_eq_zero, isEquivalent_atBot_div, IsMonicOfDegree.natDegree_eq, coe_lt_degree, IsPrimitiveRoot.totient_le_degree_minpoly, one_le_pow_mul_abs_eval_div, natDegree_eq_zero_of_derivative_eq_zero, IsAdjoinRootMonic.coeff_apply, natDegree_le_natDegree, finrank_quotient_span_eq_natDegree_norm, natDegree_monomial_le, eraseLead_natDegree_lt_or_eraseLead_eq_zero, NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply', natDegree_X, natDegree_of_subsingleton, FirstOrder.Field.realize_genericMonicPolyHasRoot, eraseLead_support, IsMonicOfDegree.natDegree_sub_X_pow, natDegree_minpolyDiv_succ, Cubic.natDegree_of_b_ne_zero, card_roots_sub_C', aeval_iterate_derivative_of_ge, MvPolynomial.natDegree_finSuccEquiv, le_natDegree_of_mem_supp, natDegree_mul_X, natDegree_X_pow_sub_C, isMonicOfDegree_iff, degree_eq_natDegree, IsAdjoinRootMonic.finrank, IsDistinguishedAt.map_eq_X_pow, le_natDegree_of_coe_le_degree, natDegree_smul, Cubic.natDegree_of_c_ne_zero, Mathlib.Tactic.ComputeDegree.natDegree_zero_le, PowerBasis.ofAdjoinEqTop'_dim, abc, finrank_quotient_span_eq_natDegree', natDegree_C_add, IsMonicOfDegree.natDegree_sub_lt, eraseLead_add_C_mul_X_pow, coeff_natDegree, natDegree_mul_mirror, aeval_sumIDeriv, WeierstrassCurve.natDegree_Ξ¨Sq, Monic.natDegree_pow, IsAlgClosed.card_roots_eq_natDegree, natDegree_pos_of_not_isUnit_of_dvd_monic, coeff_taylor_natDegree, length_coeffList_eq_ite, flt_catalan, Separable.natSepDegree_eq_natDegree, WeierstrassCurve.natDegree_preΞ¨β_pos, Lagrange.natDegree_nodal, IsAdjoinRootMonic.powerBasis_dim, Monic.natDegree_pos_of_not_isUnit, natDegree_mul, natSepDegree_eq_zero_iff, scaleRoots_evalβ_mul, natDegree_notMem_eraseLead_support, natDegree_hilbertPoly_of_ne_zero_of_rootMultiplicity_lt, natDegree_eraseLead_add_one, IsPrimitiveRoot.powerBasis_dim, self_sub_monomial_natDegree_leadingCoeff, natDegree_finset_prod_X_sub_C_eq_card, natDegree_divByMonic, natDegree_sum_le, integralNormalization_coeff_natDegree, natDegree_eq_card_roots', FunctionField.inftyValuation.polynomial, natDegree_cyclotomic, natDegree_of_dvd_cyclotomic_of_irreducible, Monic.natDegree_eq_zero, isEquivalent_atTop_lead, AdjoinRoot.powerBasis'_dim, natDegree_modByMonic_le, contraction_degree_eq_or_insep, natDegree_smul_of_smul_regular, LindemannWeierstrass.exp_polynomial_approx, Monic.eq_X_pow_iff_natDegree_le_natTrailingDegree, natDegree_prod', WeierstrassCurve.Affine.natDegree_polynomial, natDegree_prod, IsAdjoinRootMonic.basis_repr, FirstOrder.Field.lift_genericMonicPoly, natDegree_map_eq_iff, prod_roots_eq_coeff_zero_of_monic_of_splits, eraseLead_natDegree_le, natDegree_eq_one, natDegree_comp, resultant_self_eq_zero, card_eq_of_natDegree_le_of_coeff_le, eraseLead_coeff, coeff_le_of_roots_le, scaleRoots_evalβ_mul_of_commute, UniversalFactorizationRing.jacobian_resentation, card_rootSet_eq_natDegree_iff_of_splits, IsAlgClosed.card_roots_map_eq_natDegree_of_isUnit_leadingCoeff, natDegree_pos_of_evalβ_root, natDegree_mul_leadingCoeff_self_inv, PowerSeries.IsWeierstrassFactorizationAt.natDegree_eq_toNat_order_map_of_ne_top, Splits.coeff_zero_eq_prod_roots_of_monic, denomsClearable_natDegree, coeff_zero_eq_leadingCoeff_mul_prod_roots_of_splits, WeierstrassCurve.natDegree_preΞ¨_pos, Splits.natDegree_le_one_of_irreducible, natDegree_prod_le, Sequence.natDegree_strictMono, natDegree_toSubring, minpoly.two_le_natDegree_iff, natDegree_map, natDegree_lt_natDegree_iff, WeierstrassCurve.natDegree_Ξ¨βSq_pos, natDegree_C_mul_X, finrank_quotient_span_eq_natDegree, natSepDegree_eq_natDegree_of_separable, PowerBasis.natDegree_minpolyGen, exists_monic_aeval_eq_zero_forall_mem_pow_of_isIntegral, fwdDiff_iter_degree_add_one_eq_zero, natDegree_X_add_C, coeffList_eraseLead, trinomial_natDegree, FiniteField.card_image_polynomial_eval, natDegree_removeFactor, WeierstrassCurve.natDegree_Ξ¦_le, natDegree_comp_eq_of_mul_ne_zero, bUnion_roots_finite, Mathlib.Tactic.ComputeDegree.natDegree_natCast_le, resultant_dvd_leadingCoeff_pow, natDegree_lt_iff_degree_lt, natDegree_C_mul_eq_of_mul_eq_one, IsMonicOfDegree.exists_natDegree_lt, HasSeparableContraction.dvd_degree, natDegree_C, Monic.eq_X_pow_iff_natTrailingDegree_eq_natDegree, Algebra.adjoin.powerBasis_dim, WeierstrassCurve.natDegree_preΞ¨'_pos, natDegree_add_eq_left_of_degree_lt, exists_iterate_derivative_eq_factorial_smul, natDegree_minpolyDiv_lt, natDegree_list_sum_le, WeierstrassCurve.natDegree_Ξ¨Sq_le, natDegree_C_mul_le, natDegree_eq_support_max', natDegree_C_mul_of_mul_ne_zero, natDegree_mul', coeff_modByMonic_mem_pow_natDegree_mul, spectralNorm.spectralNorm_pow_natDegree_eq_prod_roots, coeff_scaleRoots, natDegree_pos_of_nextCoeff_ne_zero, div_wf_lemma, exists_approx_polynomial_aux, natDegree_scaleRoots, IsAlgClosed.card_roots_map_eq_natDegree_from_simpleRing, HasSeparableContraction.eq_degree, natDegree_modByMonic_lt, natDegree_hasseDeriv_le, natDegree_divX_le, Monic.natDegree_eq_zero_iff_eq_one, Mathlib.Tactic.ComputeDegree.natDegree_intCast_le, coeff_pow_mul_natDegree, valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X, as_sum_range, PowerSeries.IsWeierstrassFactorization.natDegree_eq_toNat_order_map, degree_erase_lt, natDegree_mul_C_eq_of_mul_eq_one, natDegree_integralNormalization, Cubic.natDegree_of_a_ne_zero, HasSeparableContraction.dvd_degree', Matrix.charmatrix_apply_natDegree, natDegree_quadratic_le, Cubic.natDegree_of_b_eq_zero', nextCoeff_eq_zero, natDegree_taylor, natSepDegree_eq_natDegree_iff, isUnit_resultant_iff_isCoprime, ite_le_natDegree_coeff, Algebra.adjoin.powerBasis'_dim, valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X, lt_natDegree_of_mem_eraseLead_support, natDegree_reflect_le, natDegree_map_eq_of_isUnit_leadingCoeff, Lagrange.natDegree_basisDivisor_self, supp_subset_range_natDegree_succ, two_le_natDegree_of_nextCoeff_eraseLead, natDegree_primPart, degree_le_natDegree, natDegree_X_pow_add_C, natDegree_pos_of_eraseLead_ne_zero, eq_C_coeff_zero_iff_natDegree_eq_zero, Chebyshev.natDegree_U_neg_one, isEquivalent_atTop_div, natDegree_add_coeff_mul, Cubic.natDegree_of_c_eq_zero, natDegree_zero, WeierstrassCurve.natDegree_preΞ¨β, comp_neg_X_leadingCoeff_eq, natDegree_eq_of_degree_eq_some, IsAlgClosed.roots_eq_zero_iff_natDegree_eq_zero, coeff_natDegree_succ_eq_zero, WeierstrassCurve.natDegree_Ξ¦, natDegree_le_of_dvd, eraseLead_add_monomial_natDegree_leadingCoeff, natDegree_X_sub_C, natDegree_hilbertPoly_of_ne_zero, resultant_scaleRoots, natDegree_C_mul, PowerBasis.mem_span_pow, natDegree_multiset_prod, card_supp_le_succ_natDegree, splits_iff_card_roots, Cubic.natDegree_of_a_eq_zero', isEquivalent_atBot_lead, natDegree_derivative_le, natDegree_C_mul_X_pow, C_mul_X_pow_eq_self, degree_eq_iff_natDegree_eq_of_pos, cardPowDegree_apply, sumIDeriv_apply, WeierstrassCurve.natDegree_Ξ¨Sq_pos, Cubic.natDegree_of_c_eq_zero', natDegree_eq_natDegree, resultant_taylor, IsAlgClosed.card_aroots_eq_natDegree, natDegree_hasseDeriv, AdjoinRoot.powerBasisAux'_repr_symm_apply, natDegree_mul_C_of_isUnit, IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree, reverse_natDegree_le, natDegree_radical_le, Monic.irreducible_iff_natDegree, isMonicOfDegree_iff', RatFunc.intDegree_add, card_roots', ascPochhammer_natDegree, mul_scaleRoots, natDegree_iterate_comp, Submodule.span_range_natDegree_eq_adjoin, IsAlgClosed.card_aroots_eq_natDegree_of_leadingCoeff_ne_zero, coeff_scaleRoots_natDegree, leadingCoeff_comp, WeierstrassCurve.natDegree_preΞ¨β_le, mirror_natDegree, Splits.natDegree_eq_card_roots, IntermediateField.card_algHom_adjoin_integral, natDegree_multiset_prod_X_sub_C_eq_card, IsPrimitiveRoot.subOnePowerBasis_dim, MvPolynomial.natDegree_optionEquivLeft, natDegree_cyclotomic_le, Cubic.natDegree_of_a_eq_zero, natDegree_one, descPochhammer_natDegree, IsPurelyInseparable.minpoly_natDegree_eq, RatFunc.intDegree_polynomial, card_roots_map_le_natDegree, SplittingFieldAux.instIsSplittingFieldNatDegree, Chebyshev.natDegree_U, natDegree_sub, natDegree_X_pow_mul, Mathlib.Tactic.ComputeDegree.natDegree_C_le, Lagrange.natDegree_basisDivisor_of_ne, Liouville.exists_pos_real_of_irrational_root, natDegree_monomial, card_rootSet_eq_natDegree, WeierstrassCurve.natDegree_Ξ¨β_le, natDegree_X_pow_le, coeff_divModByMonicAux_mem_span_pow_mul_span, WeierstrassCurve.natDegree_Ξ¨β_pos, LieAlgebra.engel_isBot_of_isMin.lieCharpoly_coeff_natDegree, WeierstrassCurve.natDegree_preΞ¨_le, natDegree_pow_le, natDegree_pow, natDegree_mul_C_eq_of_mul_ne_zero, Monic.natDegree_map, WeierstrassCurve.natDegree_Ξ¨β, natDegree_X_pow, reverse_add_C, AlgebraicClosure.Monics.map_eq_prod, Sequence.natDegree_eq, eval_sumIDeriv_of_pos, natDegree_smul_le, Matrix.charpoly_natDegree_eq_dim, IsAlgClosed.card_roots_map_eq_natDegree_of_injective, FiniteField.X_pow_card_sub_X_natDegree_eq, PowerBasis.ofGenMemAdjoin'_dim, natTrailingDegree_le_natDegree, natDegree_preHilbertPoly, IsIntegral.mem_span_pow, natDegree_add_eq_right_of_degree_lt, spectralNorm.spectralNorm_eq_norm_coeff_zero_rpow, coeff_mem_radical_span_coeff_of_dvd, Splits.natDegree_eq_one_of_irreducible, Algebra.normalizedTrace_minpoly, Field.primitive_element_iff_minpoly_natDegree_eq, IsSeparableContraction.natSepDegree_eq, WeierstrassCurve.natDegree_preΞ¨', natDegree_map_of_leadingCoeff_ne_zero, natDegree_wronskian_lt_add, AdjoinRoot.powerBasis_dim, natDegree_natCast, Irreducible.natSepDegree_dvd_natDegree, exists_monic_aeval_eq_zero_forall_mem_pow_of_mem_map, resultant_eq_prod_roots_sub, natDegree_X_sub_C_le, RatFunc.natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree, Irreducible.natDegree_pos, natDegree_freeMonic, aeval_eq_sum_range, sum_over_range, Matrix.charpoly.univ_natDegree, natDegree_eraseLead, natDegree_linear_le, natDegree_det_X_add_C_le, IsAlgClosed.card_roots_map_eq_natDegree_of_leadingCoeff_ne_zero, natDegree_map_le, supNorm_le_choose_natDegree_div_two_mul_mahlerMeasure, Chebyshev.natDegree_T, minpoly.neg, MonicDegreeEq.natDegree, Cubic.natDegree_of_zero, resultant_deriv, natDegree_modByMonic_le_left, natDegree_eq_of_degree_eq, integralNormalization_coeff_degree_ne, Splits.coeff_zero_eq_leadingCoeff_mul_prod_roots, natDegree_X_le, flt, Monic.coeff_natDegree, Matrix.charmatrix_apply_natDegree_le, eraseLead_coeff_natDegree, NumberField.hermiteTheorem.natDegree_le_rankOfDiscrBdd, cardPowDegree_nonzero, LinearMap.charpoly_natDegree, coeff_divByMonic_mem_pow_natDegree_mul, natDegree_sub_C, fwdDiff_iter_degree_eq_factorial, hasseDeriv_natDegree_eq_C, WeierstrassCurve.natDegree_preΞ¨'_le, as_sum_range_C_mul_X_pow, Mathlib.Tactic.ComputeDegree.natDegree_one_le, minpoly.natDegree_le, PowerBasis.ofAdjoinEqTop_dim, IsAlgClosed.card_aroots_eq_natDegree_of_isUnit_leadingCoeff, ncard_rootSet_le, eraseLead_natDegree_lt, RatFunc.eq_C_iff, natDegree_eq_zero_iff_degree_le_zero, eval_eq_sum_range, natDegree_mul_C_le, Monic.natDegree_mul, natDegree_of_mem_normalizedFactors_cyclotomic, card_le_degree_of_subset_roots, natDegree_mem_support_of_nonzero, natDegree_mul_C, FiniteField.X_pow_card_pow_sub_X_natDegree_eq, natDegree_restriction, natDegree_le_of_degree_le, integralNormalization_coeff, natDegree_cubic, minpoly.natDegree_eq_one_iff, natDegree_C_mul_of_isUnit, Monic.irreducible_iff_natDegree', natDegree_shiftedLegendre, AdjoinRoot.powerBasisAux'_repr_apply_to_fun, IsAdjoinRootMonic.coeff_apply_coe, coeff_mirror, Monic.mul_natDegree_lt_iff, Monic.natDegree_mul_comm, PowerBasis.dim_le_natDegree_of_root, natDegree_mul_le, WeierstrassCurve.natDegree_Ξ¨βSq, natDegree_map_eq_of_injective, Cubic.natDegree_of_b_ne_zero', natDegree_coe_units, evalβ_eq_sum_range, Monic.natDegree_pos, natDegree_neg, IsSeparableContraction.degree_eq, natDegree_intCast, evalβ_reverse_mul_pow, natDegree_iterate_derivative, exists_prod_multiset_X_sub_C_mul, scaleRoots_zero, natDegree_opRingEquiv, natDegree_multiset_prod', dvd_pow_natDegree_of_evalβ_eq_zero, natDegree_prod_of_monic, natDegree_monomial_eq, isUnitTrinomial_iff', resultant_self, le_natDegree_of_ne_zero, reverse_natDegree, withBotSucc_degree_eq_natDegree_add_one, natDegree_expand, one_lt_natDegree_of_irrational_root, MvPolynomial.degreeOf_eq_natDegree, spectralValue_eq_zero_iff, natDegree_multiset_prod_le, LieAlgebra.engel_isBot_of_isMin.lieCharpoly_natDegree, natDegree_cyclotomic', coeff_mul_mirror, natDegree_eq_zero_of_isUnit, natDegree_mod_lt, Cubic.natDegree_of_c_ne_zero', LinearMap.polyCharpoly_natDegree, lifts_and_natDegree_eq_and_monic, natDegree_pos_iff_degree_pos, monomial_natDegree_leadingCoeff_eq_self, minpoly.degree_dvd, linearIndependent_pow, eraseLead_natDegree_le_aux, natDegree_comp_le, natDegree_eraseLead_le_of_nextCoeff_eq_zero, degree_eq_iff_natDegree_eq, Monic.as_sum, natDegree_eq_card_roots, norm_coeff_le_choose_mul_mahlerMeasure, WeierstrassCurve.natDegree_Ξ¨βSq_le, natDegree_derivative_lt, minpoly.natDegree_pos, PowerBasis.natDegree_minpoly, natDegree_lt_natDegree, Cubic.natDegree_of_a_ne_zero', finite_mahlerMeasure_le, IsAdjoinRootMonic.deg_pos, natDegree_ofNat, coeff_reverse, natDegree_le_iff_degree_le, Lagrange.natDegree_basis, natDegree_multiset_prod_of_monic, integralNormalization_coeff_ne_natDegree, reverse_C_add, supDegree_eq_natDegree, natDegree_linear, natDegree_X_mul, coeff_comp_degree_mul_degree, natDegree_sub_le, natDegree_pow_X_add_C, LaurentPolynomial.toLaurent_reverse, natDegree_eq_zero, scaleRoots_eval_mul, natDegree_sub_eq_of_prod_eq, coeff_divByMonic_X_sub_C, resultant_eq_zero_iff, natDegree_cubic_le, coeff_mul_degree_add_degree, content_eq_gcd_range_succ, natDegree_pos_of_aeval_root, natDegree_quadratic, natDegree_divX_eq_natDegree_tsub_one, natDegree_C_mul_X_pow_le, natDegree_map_lt, dvd_pow_natDegree_of_aeval_eq_zero, PowerSeries.natDegree_trunc_lt, natDegree_eq_reverse_natDegree_add_natTrailingDegree, self_sub_C_mul_X_pow, natDegree_add_C, ofFn_natDegree_lt, resultant_integralNormalization, int_natDegree, homogenize_dvd, IntermediateField.adjoin.powerBasis_dim, card_mahlerMeasure_le_prod, degree_list_sum_le, IsDistinguishedAt.coe_natDegree_eq_order_map, minpoly.two_le_natDegree_subalgebra, coeff_natDegree_eq_zero_of_degree_lt, natDegree_list_prod_le, natDegree_pow', LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul, Chebyshev.natDegree_U_natCast, MvPolynomial.universalFactorizationMapPresentation_jacobian, coeff_zero_eq_prod_roots_of_monic_of_splits, natDegree_multiset_sum_le, natDegree_minpolyDiv, Monic.neg_one_pow_natDegree_mul_comp_neg_X, Cubic.natDegree_of_b_eq_zero, WeierstrassCurve.natDegree_Ξ¦_pos, Monic.natDegree_mul', WeierstrassCurve.natDegree_preΞ¨, natDegree_add_le, aeval_sumIDeriv_of_pos, IsAdjoinRootMonic.basis_apply, IsSeparableContraction.dvd_degree'
|
nextCoeff π | CompOp | 31 mathmath: nextCoeff_map, prod_X_sub_C_nextCoeff, Splits.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff, nextCoeff_of_natDegree_pos, nextCoeff_C_mul_X_add_C, nextCoeff_mul_C, nextCoeff_X_add_C, PowerBasis.trace_gen_eq_nextCoeff_minpoly, trace_eq_finrank_mul_minpoly_nextCoeff, Monic.nextCoeff_mul, nextCoeff_eq_zero, nextCoeff_C_eq_zero, Splits.nextCoeff_eq_neg_sum_roots_of_monic, nextCoeff_X_sub_C, Matrix.trace_eq_neg_charpoly_nextCoeff, Monic.nextCoeff_multiset_prod, multiset_prod_X_sub_C_nextCoeff, sum_roots_eq_nextCoeff_of_monic_of_split, nextCoeff_map_eq, nextCoeff_eq_neg_sum_roots_of_monic_of_splits, Algebra.normalizedTrace_minpoly, nextCoeff_map_of_leadingCoeff_ne_zero, coeff_one_reverse, leadingCoeff_eraseLead_eq_nextCoeff, Monic.nextCoeff_pow, nextCoeff_eq_zero_of_eraseLead_eq_zero, nextCoeff_map_eq_of_isUnit_leadingCoeff, Monic.nextCoeff_prod, nextCoeff_C_mul, trace_adjoinSimpleGen, nextCoeff_eq_neg_sum_roots_mul_leadingCoeff_of_splits
|