| Name | Category | Theorems |
|---|
C π | CompOp | 806 mathmath: mul_div_eq_iff_isRoot, not_ker_le_map_C_of_surjective_of_quasiFiniteAt, isUnit_C_add_X_mul_iff, isMonicOfDegree_X_add_one, natDegree_mul_leadingCoeff_inv, ker_mapRingHom, X_pow_mul_assoc_C, separable_X_add_C, mahlerMeasure_const, eq_X_sub_C_of_separable_of_root_eq, eq_C_of_derivative_eq_zero, derivative_X_sq, coe_normUnit_of_ne_zero, separable_X_pow_sub_C_unit, splits_iff_exists_multiset, taylorWithin_succ, MvPolynomial.pUnitAlgEquiv_apply, algEquivCMulXAddC_apply, mul_divByMonic_eq_iff_isRoot, monic_X_sub_C, RatFunc.num_div, mem_image_comap_C_basicOpen, ker_evalRingHom, StandardEtalePair.inv_aeval_X_g, IsPurelyInseparable.minpoly_eq', expand_eq_sum, root_X_sub_C, AlgebraicGeometry.Polynomial.isOpenMap_comap_C, X_pow_sub_C_splits_of_isPrimitiveRoot, Differential.implicitDeriv_C, WeierstrassCurve.Affine.CoordinateRing.smul, resultant_X_add_C_right, pow_rootMultiplicity_dvd, AdjoinRoot.minpoly_root, X_pow_sub_C_eq_prod, rootMultiplicity_eq_rootMultiplicity, derivative_C_mul, support_trinomial, AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_symm_mk, rootMultiplicity_eq_natTrailingDegree, div_def, Cubic.of_a_eq_zero', C_inj, prod_X_sub_C_nextCoeff, mem_roots_sub_C', Monic.leadingCoeff_C_mul, Ideal.mem_leadingCoeffNth_zero, leadingCoeff_quadratic, Multiset.prod_X_sub_X_eq_sum_esymm, coeffList_C_mul, support_C_mul_X, ChevalleyThm.chevalley_polynomialC, nnqsmul_eq_C_mul, leadingCoeff_C_mul_of_isUnit, aroots_X_sub_C, fiberEquivQuotient_tmul, MvPolynomial.optionEquivLeft_C, degree_quadratic_lt, AlgebraicGeometry.Polynomial.comap_C_mem_imageOfDf, C_mul_X_eq_monomial, eval_det_add_X_smul, prod_multiset_X_sub_C_of_monic_of_roots_card_eq, logMahlerMeasure_C_mul, C_1, WeierstrassCurve.Οβ_sq, MvPolynomial.optionEquivLeft_X_some, monic_X_pow_add_C, monic_multisetProd_X_sub_C, isCoprime_of_is_root_of_eval_derivative_ne_zero, leadingCoeff_det_X_one_add_C, quotientSpanXSubCAlgEquiv_symm_apply, X_pow_sub_C_irreducible_iff_of_odd, zero_notMem_multiset_map_X_sub_C, card_roots_sub_C', Irreducible.natSepDegree_eq_one_iff_of_monic', eq_C_of_degree_eq_zero, nextCoeffUp_C_eq_zero, X_pow_sub_C_irreducible_of_odd, derivative_pow_succ, StandardEtalePresentation.toPresentation_algebra_smul, minpoly.eq_of_irreducible, Ideal.quotient_map_C_eq_zero, natDegree_X_pow_sub_C, Monic.natSepDegree_eq_one_iff_of_irreducible', AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C, roots_C_mul_X_pow, iterate_derivative_eq_factorial_smul_sum, iterate_derivative_X_add_pow, Chebyshev.S_eq_U_comp_half_mul_X, degree_C_mul_of_isUnit, aroots_quadratic_eq_pair_iff_of_ne_zero', degree_mul_leadingCoeff_inv, eq_prod_roots_of_splits, eq_prod_roots_of_monic_of_splits_id, WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_C, MvPolynomial.optionEquivLeft_apply, minpoly_algHom_toLinearMap, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_eqβ, prime_C_iff, Lagrange.interpolate_eq_nodalWeight_mul_nodal_div_X_sub_C, natSepDegree_X_sub_C_pow, isMonicOfDegree_two_iff', not_isRoot_C, Multiset.prod_X_add_C_coeff, natDegree_C_add, Monic.eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one, C_mul', eraseLead_add_C_mul_X_pow, minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C, isMonicOfDegree_X_sub_one, ConjRootClass.minpoly.map_eq_prod, sumIDeriv_C, roots_C_mul, coeff_divByMonic_X_sub_C_rec, leadingCoeff_X_pow_add_C, eval_C, Matrix.charmatrix_apply_eq, Lagrange.nodal_insert_eq_nodal, mapAlgHom_eq_evalβAlgHom'_CAlgHom, eval_divByMonic_eq_trailingCoeff_comp, algebraMap_apply, MvPolynomial.optionEquivRight_C, monomial_mul_C, X_pow_sub_C_irreducible_iff_forall_prime_of_odd, as_sum_range_C_mul_X_pow', Matrix.derivative_det_one_add_X_smul, integralNormalization_C, rootMultiplicity_X_sub_C_pow, resultant_X_sub_C_right, update_eq_add_sub_coeff, monic_finprod_X_sub_C, degree_C_mul_of_mul_ne_zero, Ideal.jacobson_bot_polynomial_le_sInf_map_maximal, Real.Polynomial.isRoot_cos_pi_div_five, coe_C, WeierstrassCurve.Affine.C_addPolynomial, natDegree_finset_prod_X_sub_C_eq_card, support_C_mul_X', pow_rootMultiplicity_not_dvd, divByMonic_add_X_sub_C_mul_derivative_divByMonic_eq_derivative, Bivariate.aveal_eq_map_swap, le_trailingDegree_C, Bivariate.swap_apply, Ideal.injective_quotient_le_comap_map, C_eq_zero, dvd_comp_X_add_C_iff, separable_X_pow_sub_C, dvd_comp_C_mul_X_add_C_iff, X_pow_sub_one_splits, coeff_C_ne_zero, isMonicOfDegree_add_add_two, degree_X_pow_add_C, Matrix.det_one_add_smul, Monic.comp_X_sub_C, degree_X_sub_C, iterate_derivative_X_sub_pow, support_trinomial', C_0, isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top, exists_finset_of_splits, Submodule.IsPrincipal.contentIdeal_le_span_iff_dvd, Matrix.charpoly_of_upperTriangular, irreducible_mul_leadingCoeff_inv, IsSepClosed.roots_eq_zero_iff, gal_X_pow_sub_C_isSolvable, Lagrange.interpolate_eq_sum, Module.AEval.C_smul, sum_C_index, Matrix.charmatrix_apply_ne, natTrailingDegree_C, X_mul_C, Derivation.mapCoeffs_C, coeff_C_mul_X, leadingCoeff_cubic, resultant_C_zero_right, natDegree_eq_one, minpoly.sub_algebraMap, WeierstrassCurve.Ο_three, C_eq_natCast, derivative_X_sub_C_sq, Matrix.charpoly_sub_scalar, smul_eq_C_mul, opRingEquiv_op_C, C_eq_intCast, degree_C_lt_degree_C_mul_X, aroots_C_mul, isUnit_iff, roots_X_pow_char_pow_sub_C_pow, Multiset.prod_X_sub_C_dvd_iff_le_roots, leadingCoeff_mul_prod_normalizedFactors, Matrix.IsHermitian.charpoly_cfc_eq, mem_span_C_X_sub_C_X_sub_C_iff_eval_eval_eq_zero, nextCoeff_C_mul_X_add_C, prod_multiset_root_eq_finset_root, dvd_C_mul, X_pow_sub_C_separable_iff, IsPurelyInseparable.minpoly_eq, nextCoeff_mul_C, coeff_X_sub_C_mul, Cubic.of_a_eq_zero, comp_C_mul_X_eq_zero_iff, gal_X_pow_sub_C_isSolvable_aux, degree_quadratic, monic_X_pow_sub_C, leadingCoeff_linear, rootMultiplicity_eq_natFind_of_ne_zero, isMonicOfDegree_two_iff, C_mul_X_pow_eq_monomial, nextCoeff_X_add_C, StandardEtalePair.equivMvPolynomialQuotient_symm_apply, PowerSeries.trunc_mul_C, eq_X_add_C_of_degree_le_one, expand_C, logMahlerMeasure_X_sub_C, C_mem_lifts, natDegree_mul_leadingCoeff_self_inv, CAlgHom_apply, trailingDegree_C_mul_X_pow, X_pow_sub_one_eq_prod, prod_multiset_X_sub_C_dvd, degree_cubic_lt, AdjoinRoot.mul_div_root_cancel, eq_X_add_C_of_natDegree_le_one, minpoly.natSepDegree_eq_one_iff_eq_X_sub_C_pow, degree_C, Cubic.of_b_eq_zero, derivative_X_add_C, WeierstrassCurve.Affine.CoordinateRing.C_addPolynomial, support_binomial', minpoly.IsIntegrallyClosed.isIntegral_iff_leadingCoeff_dvd, exists_image_comap_of_monic, cyclotomic_eq_prod_X_sub_primitiveRoots, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_add_eq, X_add_C_scaleRoots, resultant_C_right, splits_C, Splits.comp_X_sub_C, WeierstrassCurve.Ξ¨_ofNat, natDegree_C_mul_X, comp_C, coeff_mul_X_sub_C, RatFunc.numDenom_div, natDegree_X_add_C, map_under_lt_comap_of_weaklyQuasiFiniteAt, support_C, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C', natSepDegree_C_mul_X_sub_C_pow, height_map_C, RatFunc.num_C, X_sub_C_mul_divByMonic_eq_sub_modByMonic, roots_C_mul_X_sub_C_of_IsUnit, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk, derivative_X_pow_succ, eq_C_of_natDegree_le_zero, monic_X_add_C, logMahlerMeasure_X_add_C, aevalTower_C, WeierstrassCurve.Affine.addPolynomial_slope, coeff_C_mul, rootMultiplicity_eq_nat_find_of_nonzero, roots_quadratic_eq_pair_iff_of_ne_zero, derivative_X_sub_C_pow, natDegree_C_mul_eq_of_mul_eq_one, eraseLead_C_mul_X, natDegree_C, X_pow_sub_C_irreducible_iff_of_prime_pow, Lagrange.basis_eq_prod_sub_inv_mul_nodal_div, toLaurent_comp_C, IsRoot.mul_div_eq, sum_C_mul_X_pow_eq, isOpen_image_comap_of_monic, as_sum_support_C_mul_X_pow, degree_quadratic_le, eq_quadratic_of_degree_le_two, WeierstrassCurve.Ο_one, divX_eq_zero_iff, MulSemiringAction.charpoly_eq_prod_smul, card_support_eq, leadingCoeff_pow_X_add_C, AlgebraicGeometry.Polynomial.imageOfDf_eq_comap_C_compl_zeroLocus, cauchyBound_C, roots_C_mul_X_add_C, natDegree_C_mul_le, leadingCoeff_X_pow_sub_C, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some, Bivariate.equivMvPolynomial_symm_X_0, minpoly.eq_X_sub_C_of_algebraMap_inj, taylor_apply, natDegree_C_mul_of_mul_ne_zero, WeierstrassCurve.Affine.C_addPolynomial_slope, Splits.eq_prod_roots, evalEvalRingHom_apply, div_wf_lemma, Matrix.charmatrix_fromBlocks, eq_X_add_C_of_degree_eq_one, mahlerMeasure_C_mul_X_add_C, eq_C_of_natDegree_eq_zero, evalβ_C_X, smeval_C, mem_span_C_coeff, WeierstrassCurve.Affine.CoordinateRing.norm_smul_basis, X_mul_divX_add, card_support_binomial, separable_C_mul_X_pow_add_C_mul_X_add_C', Splits.comp_X_add_C, C_mul_monomial, monic_C_mul_of_mul_leadingCoeff_eq_one, separable_X_pow_sub_C', isOpenMap_comap_C, natDegree_mul_C_eq_of_mul_eq_one, content_C_mul, Splits.eq_X_sub_C_of_single_root, coeff_det_X_add_C_card, quotientSpanXSubCAlgEquiv_mk, Cubic.of_c_eq_zero', Lagrange.X_sub_C_dvd_nodal, roots_X_sub_C, isUnit_C, WeierstrassCurve.C_Ξ¨βSq, natDegree_quadratic_le, Bivariate.swap_Y, rootSet_C_mul_X_pow, le_rootMultiplicity_iff, support_C_subset, Cubic.of_b_eq_zero', WeierstrassCurve.Affine.derivative_addPolynomial_slope, support_C_mul_X_pow', eq_C_content_mul_primPart, C'_mem_lifts, rootMultiplicity_mul_X_sub_C_pow, card_support_eq', C_eq_algebraMap, Finset.prod_X_add_C_coeff, Bivariate.equivMvPolynomial_symm_C, divX_mul_X_add, natSepDegree_X_pow_char_pow_sub_C, coeffList_C, Matrix.det_one_add_X_smul, comp_eq_zero_iff, RatFunc.smul_eq_C_smul, degree_X_pow_sub_C, Irreducible.natSepDegree_eq_one_iff_of_monic, natDegree_X_pow_add_C, divX_C_mul, iterate_derivative_C, degree_mul_leadingCoeff_self_inv, mahlerMeasure_X_add_C, taylor_X_pow, eq_C_coeff_zero_iff_natDegree_eq_zero, Differential.mapCoeffs_C, comp_C_mul_X_coeff, gal_C_isSolvable, resultant_X_sub_C_pow_left, derivative_C_mul_X, Bivariate.swap_X, eval_iterate_derivative_rootMultiplicity, Splits.X_add_C, degree_C_lt, nextCoeff_C_eq_zero, degree_C_mul_X_pow_le, separable_prod_X_sub_C_iff', le_trailingDegree_C_mul_X_pow, AdjoinRoot.root_isInv, PowerSeries.trunc_one_left, coeff_mul_C, rootMultiplicity_C, eq_prod_roots_of_splits_id, coeff_C, natDegree_X_sub_C, WeierstrassCurve.Affine.CoordinateRing.mk_Ο, Matrix.matPolyEquiv_charmatrix, natDegree_C_mul, card_support_eq_three, resultant_X_sub_C_pow_right, smeval_C_mul, X_sub_C_dvd_sub_C_eval, WeierstrassCurve.Ξ¨_three, prime_X_sub_C, Lagrange.iterate_derivative_interpolate, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, C_sub, roots_X_pow_char_sub_C_pow, Bivariate.swap_C_C, isCompact_image_comap_of_monic, iterate_derivative_eq_sum, quadratic_dvd_of_aeval_eq_zero_im_ne_zero, algEquivAevalXAddC_symm_apply, isMaximal_comap_C_of_isJacobsonRing, nextCoeff_X_sub_C, natDegree_C_mul_X_pow, dvd_mul_leadingCoeff_inv, RatFunc.algebraMap_C, C_mul_X_pow_eq_self, degree_X_sub_C_le, PowerSeries.trunc_C, degree_C_mul_X_le, expand_zero, quotient_mk_comp_C_isIntegral_of_isJacobsonRing, eraseLead_C_mul_X_pow, Monic.natSepDegree_eq_one_iff, trailingDegree_C, X_pow_sub_C_irreducible_of_prime, roots_multiset_prod_X_sub_C, homogenize_C_mul, contract_C, Matrix.charpoly_fin_two, evalβ_mul_C', separable_prod_X_sub_C_iff, resultant_C_left, natDegree_mul_C_of_isUnit, dickson_add_two, exists_eq_pow_rootMultiplicity_mul_and_not_dvd, Bivariate.swap_map_C, Monic.eq_X_add_C, WeierstrassCurve.Affine.CoordinateRing.mk_Ξ¨_sq, mapRingHom_comp_C, eq_C_of_degree_le_zero, contentIdeal_C, eval_C_X_evalβ_map_C_X, supNorm_C, matPolyEquiv_map_C, card_roots_X_pow_sub_C, derivative_sq, leadingCoeff_C_mul_X_pow, mem_roots_sub_C, RatFunc.liftRingHom_C, isMaximal_comap_C_of_isMaximal, not_isUnit_X_add_C, degree_cubic, natSepDegree_C_mul, isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_neg_mul, resultant_X_add_C_left, gal_X_sub_C_isSolvable, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_eqβ, IsMonicOfDegree.aeval_add, natDegree_multiset_prod_X_sub_C_eq_card, C_dvd_iff_dvd_coeff, Splits.C_mul_X_pow, exists_eq_X_add_C_of_natDegree_le_one, Matrix.charpoly_coeff_eq_prod_coeff_of_le, AdjoinRoot.Polynomial.quotQuotEquivComm_mk, RatFunc.denom_div, opRingEquiv_symm_C_mul_X_pow, iterate_derivative_prod_X_sub_C, signVariations_eraseLead_mul_X_sub_C, dvd_content_iff_C_dvd, coeff_C_succ, separable_C, instIsLocalHomRingHomC, cfc_eval_C, mahlerMeasure_X_sub_C, minpoly.add_algebraMap, not_ker_le_map_C_of_surjective_of_weaklyQuasiFiniteAt, Ideal.isPrime_map_C_of_isPrime, MvPolynomial.finSuccEquiv_comp_C_eq_C, MulSemiringAction.charpoly_eq, WeierstrassCurve.Affine.CoordinateRing.C_addPolynomial_slope, isMonicOfDegree_one_iff, root_X_pow_sub_C_pow, Mathlib.Tactic.ComputeDegree.natDegree_C_le, C_mul_dvd, MvPolynomial.finSuccEquiv_eq, C_comp, div_C, aroots_quadratic_eq_pair_iff_of_ne_zero, comp_one, Ideal.mem_map_C_iff, sumIDeriv_X, dvd_C_mul_X_sub_one_pow_add_one, rootSet_C, matPolyEquiv_symm_C, Bivariate.equivMvPolynomial_C_X, isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C, natDegree_mul_C_eq_of_mul_ne_zero, ofMultiset_apply, Cubic.prod_X_sub_C_eq, rootMultiplicity_eq_multiplicity, derivative_evalβ_C, multiset_prod_X_sub_C_nextCoeff, C_div, Lagrange.nodal_eq_mul_nodal_erase, divX_C_mul_X_pow, MvPolynomial.prod_X_add_C_coeff, WeierstrassCurve.Ο_three, Ideal.polynomialQuotientEquivQuotientPolynomial_symm_mk, derivative_pow, C_ofNat, reverse_add_C, isSplittingField_C, AlgebraicClosure.Monics.map_eq_prod, isLocalization, image_comap_C_basicOpen, dickson_one_one_eq_chebyshev_T, leadingCoeff_mul_C_of_isUnit, not_isUnit_X_sub_C, MvPolynomial.finSuccEquiv_X_succ, card_support_eq_two, eq_mul_leadingCoeff_of_monic_of_dvd_of_natDegree_le, chebyshev_T_eq_dickson_one_one, iterate_derivative_C_mul, reflect_C_mul_X_pow, card_support_eq_one, coe_expand, aroots_C_mul_X_pow, Matrix.charpoly_sub_diagonal_degree_lt, leadingCoeff_C_mul_X, eraseLead_C, Splits.X_sub_C, isUnit_primPart_C, C_leadingCoeff_mul_prod_multiset_X_sub_C, minpoly.eq_X_sub_C', Monic.comp_X_add_C, divX_C, StandardEtalePresentation.toPresentation_Ο', Monic.C_dvd_iff_isUnit, monic_mul_C_of_leadingCoeff_mul_eq_one, natSepDegree_C, IsIntegrallyClosed.eq_map_mul_C_of_dvd, monic_mul_leadingCoeff_inv, eq_X_sub_C_of_splits_of_single_root, card_support_C_mul_X_pow_le_one, discr_C, support_C_mul_X_pow, MvPolynomial.prod_C_add_X_eq_sum_esymm, modByMonic_X_sub_C_eq_C_eval, denomsClearable_C_mul_X_pow, binomial_eq_binomial, iterate_derivative_X_pow_eq_C_mul, derivative_X_pow, MvPolynomial.finSuccEquiv_apply, degree_C_mul, gaussNorm_C, Splits.eq_prod_roots_of_monic, isNilpotent_C_mul_pow_X_of_isNilpotent, leadingCoeff_X_sub_C, expand_eq_C, RatFunc.num_div_dvd', WeierstrassCurve.Ξ¦_two, aeval_C, taylor_monomial, Lagrange.interpolate_apply, IsPurelyInseparable.minpoly_eq_X_pow_sub_C, C_mul, natDegree_X_sub_C_le, splits_X_sub_C_mul_iff, dickson_of_two_le, Matrix.coeff_det_one_add_X_smul_one, degree_add_degree_leadingCoeff_inv, trinomial_def, X_sub_C_scaleRoots, resultant_C_zero_left, C_eq_or_isOpenQuotientMap_eval, sum_taylor_eq, isNilpotent_C_iff, disc_C, hasseDeriv_C, natDegree_linear_le, derivation_C, minpoly_algEquiv_toLinearMap, natDegree_det_X_add_C_le, eval_C_X_comp_evalβ_map_C_X, AdjoinRoot.algHom_subsingleton, mod_X_sub_C_eq_C_eval, StandardEtalePresentation.aeval_val_equivMvPolynomial, smul_C, AdjoinRoot.Polynomial.quotQuotEquivComm_symm_mk_mk, LinearMap.charpoly_sub_smul, Bivariate.swap_C, natSepDegree_X_sub_C, coe_normUnit, WeierstrassCurve.Affine.CoordinateRing.coe_norm_smul_basis, degree_le_zero_iff, IsAdjoinRoot.algebraMap_apply, spectralValue_X_sub_C, StandardEtalePair.aeval_X_g_mul_mk_X, roots_C_mul_X_sub_C, WeierstrassCurve.Affine.CoordinateRing.mk_Οβ_sq, rootMultiplicity_le_iff, eraseLead_mul_eq_mul_eraseLead_of_nextCoeff_zero, modByMonic_X, IsPurelyInseparable.minpoly_eq_X_sub_C_pow, X_pow_sub_C_irreducible_of_prime_pow, integralNormalization_mul_C_leadingCoeff, roots_quadratic_eq_pair_iff_of_ne_zero', iterate_derivative_X_sub_pow_self, X_dvd_sub_C, eval_mul_X_sub_C, minpolyDiv_spec, reverse_C, Splits.C_mul, Monic.eq_X_pow_char_pow_sub_C_of_natSepDegree_eq_one_of_irreducible, reflect_C, evalβ_C, comp_zero, reflect_C_mul, Matrix.charpoly_inv, natDegree_sub_C, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, hasseDeriv_natDegree_eq_C, as_sum_range_C_mul_X_pow, Submodule.IsPrincipal.contentIdeal_generator_dvd, AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_mk, derivative_C_mul_X_pow, signVariations_X_sub_C_mul_eraseLead_le, support_binomial, derivative_C, roots_X_pow_char_sub_C, degree_mul_C_of_isUnit, AdjoinRoot.minpoly_powerBasis_gen, map_under_lt_comap_of_quasiFiniteAt, dickson_two_one_eq_chebyshev_U, C_mul_comp, bernoulli_one, StandardEtalePresentation.toPresentation_val, Ideal.isDomain_map_C_quotient, natDegree_mul_C_le, Chebyshev.C_eq_two_mul_T_comp_half_mul_X, monomial_zero_left, natDegree_mul_C, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk, WeierstrassCurve.Ο_four, rootMultiplicity_X_sub_C_self, splits_X_sub_C, algEquivCMulXAddC_symm_apply, Chebyshev.T_eq_half_mul_C_comp_two_mul_X, opRingEquiv_symm_C, IsAlgClosed.roots_eq_zero_iff, natDegree_cubic, degree_leadingCoeff_inv, IsMonicOfDegree.aeval_sub, toFinsupp_C_mul_X_pow, logMahlerMeasure_const, natDegree_C_mul_of_isUnit, hermite_zero, dickson_two, succ_signVariations_X_sub_C_mul_monomial, derivative_X_add_C_sq, comp_eq_sum_left, rootMultiplicity_X_sub_C, IsLocalization.adjoin_inv, dvd_comp_X_sub_C_iff, evalEval_map_C, pow_mul_divByMonic_rootMultiplicity_eq, algEquivAevalXAddC_apply, leadingCoeff_C, cauchyBound_X_add_C, degree_cubic_le, WeierstrassCurve.Ξ¨_four, toLaurent_C_mul_eq, X_sub_C_mul_removeFactor, aevalTower_comp_C, logMahlerMeasure_C_mul_X_add_C, Cubic.eq_prod_three_roots, Multiset.prod_X_add_C_eq_sum_esymm, coeff_C_zero, exists_prod_multiset_X_sub_C_mul, degree_linear_le, Matrix.charmatrix_apply, derivative_X_add_C_pow, homogenize_C, content_C, splits_iff_exists_multiset', toFinsupp_C_mul_X, minpoly.natSepDegree_eq_one_iff_eq_expand_X_sub_C, dvd_iff_isRoot, qsmul_eq_C_mul, Multiset.prod_X_add_C_coeff', degree_linear_lt_degree_C_mul_X_sq, cauchyBound_X_sub_C, splits_of_exists_multiset, map_C, C_neg, isNilpotent_pow_X_mul_C_of_isNilpotent, prod_X_sub_C_coeff_card_pred, MvPolynomial.optionEquivLeft_symm_C_X, not_irreducible_C, degree_quadratic_lt_degree_C_mul_X_cb, coeff_C_mul_X_pow, WeierstrassCurve.Ο_two, degree_C_mul_X, comp_X_add_C_eq_zero_iff, resultant_X_sub_C_left, scaleRoots_C, degree_mul_C, div_C_mul, resultant_C_mul_left, StandardEtalePresentation.toPresentation_relation, opRingEquiv_op_C_mul_X_pow, Ideal.polynomialQuotientEquivQuotientPolynomial_map_mk, roots_X_add_C, Ideal.quotient_mk_maps_eq, mul_star_dvd_of_aeval_eq_zero_im_ne_zero, base_mul_mem_lifts, separable_C_mul_X_pow_add_C_mul_X_add_C, Matrix.IsHermitian.charpoly_eq, taylor_X, multiset_prod_X_sub_C_coeff_card_pred, separable_X_sub_C, finiteMultiplicity_X_sub_C, WeierstrassCurve.Affine.CoordinateRing.XYIdeal'_eq, leadingCoeff_X_add_C, degree_sum_fin_lt, exists_C_coeff_notMem, ringHom_ext'_iff, irreducible_X_sub_C, Monic.as_sum, preimage_eval_singleton, Cubic.C_mul_prod_X_sub_C_eq, toLaurent_C, eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le, irreducible_C_mul_X_add_C, succ_signVariations_le_X_sub_C_mul, Splits.C, reverse_C_add, natDegree_linear, autAdjoinRootXPowSubC_root, toLaurent_C_mul_X_pow, Ideal.isPrime_map_C_iff_isPrime, Matrix.charpoly_diagonal, degree_add_C, toAddCircle_C_eq_smul_fourier_zero, evalEval_C, natDegree_pow_X_add_C, natDegree_eq_zero, Monic.natSepDegree_eq_one_iff_of_irreducible, IsUnitTrinomial.irreducible_aux1, roots_C_mul_X_add_C_of_IsUnit, mirror_C, MvPolynomial.optionEquivLeft_symm_C_C, Cubic.of_c_eq_zero, matPolyEquiv_eq_X_pow_sub_C, coeff_divByMonic_X_sub_C, Matrix.derivative_det_one_add_X_smul_aux, degree_C_mul_X_pow, C_pow, C_add, zero_notMem_multiset_map_X_add_C, mod_def, leadingCoeff_divByMonic_X_sub_C, pairwise_coprime_X_sub_C, derivative_X_sub_C, aroots_C, minpoly.eq_X_sub_C, roots_C, Matrix.charmatrix_diagonal, Lagrange.nodal_erase_eq_nodal_div, monic_prod_X_sub_C, natDegree_cubic_le, WeierstrassCurve.Ο_four, Bivariate.equivMvPolynomial_C_C, WeierstrassCurve.Ξ¨_odd, natDegree_quadratic, natDegree_C_mul_X_pow_le, card_roots_sub_C, resultant_C_mul_right, degree_linear, taylor_C, derivative_apply, C_injective, nextCoeff_C_mul, self_sub_C_mul_X_pow, monomial_comp, comap_C_surjective, natDegree_add_C, eval_C_mul, isCoprime_X_sub_C_of_isUnit_sub, irreducible_X_pow_sub_C_of_root_adjoin_eq_top, signVariations_C_mul, Lagrange.interpolate_singleton, C_content_dvd, coeff_X_add_C_pow, WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_Y, degree_linear_lt, PowerSeries.trunc_C_mul, coeff_det_X_add_C_zero, PrimeSpectrum.isConstructible_comap_C, derivative_C_mul_X_sq, Lagrange.nodal_eq, derivativeFinsupp_C, card_support_trinomial, taylor_one, X_pow_sub_C_irreducible_iff_of_prime, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_mul_XYIdeal, AdjoinRoot.mk_C, roots_X_pow_char_pow_sub_C, RatFunc.algebraMap_comp_C, toMvPolynomial_C, exists_mul_add_mul_eq_C_resultant, Matrix.charpoly_of_card_eq_two, eval_multiset_prod_X_sub_C_derivative, toFinsupp_C, X_sub_C_pow_dvd_iff, isCyclic_tfae, roots_prod_X_sub_C, C_smul_derivation_apply, X_pow_mul_C, degree_sub_C, Multiset.prod_X_sub_C_coeff, degree_X_add_C, isMonicOfDegree_sub_add_two, algebraMap_eq, degree_C_le, comp_C_integral_of_surjective_of_isJacobsonRing, isIntegral_isLocalization_polynomial_quotient, Monic.eq_X_sub_C_pow_of_natSepDegree_eq_one_of_splits
|
X π | CompOp | 903 mathmath: mul_div_eq_iff_isRoot, isUnit_C_add_X_mul_iff, natDegree_mul_X_pow, isMonicOfDegree_X_add_one, degreeLT.addLinearEquiv_symm_apply_inr, X_pow_mul_assoc_C, separable_X_add_C, monic_X_pow, leadingCoeff_mul_X_pow, eq_X_sub_C_of_separable_of_root_eq, derivative_X_sq, mirror_X, separable_X_pow_sub_C_unit, splits_iff_exists_multiset, Chebyshev.T_eq_X_mul_U_sub_U, polynomialFunctions.eq_adjoin_X, taylorWithin_succ, MvPolynomial.pUnitAlgEquiv_apply, algEquivCMulXAddC_apply, mul_divByMonic_eq_iff_isRoot, LaurentPolynomial.mk'_one_X_pow, monic_X_sub_C, coeff_X_pow_mul', one_add_X_pow_sub_X_pow, eq_cyclotomic_iff, ker_evalRingHom, StandardEtalePair.inv_aeval_X_g, evalβ_intCastRingHom_X, IsPurelyInseparable.minpoly_eq', LaurentPolynomial.mk'_mul_T, expand_eq_sum, root_X_sub_C, X_pow_sub_C_splits_of_isPrimitiveRoot, Matrix.pow_eq_aeval_mod_charpoly, resultant_X_add_C_right, pow_rootMultiplicity_dvd, X_pow_sub_C_eq_prod, rootMultiplicity_eq_rootMultiplicity, ascPochhammer_one, expNegInvGlue.hasDerivAt_polynomial_eval_inv_mul, support_trinomial, divX_X_pow, KaehlerDifferential.polynomialEquiv_symm, cyclotomic_six, rootMultiplicity_eq_natTrailingDegree, Chebyshev.one_sub_X_sq_mul_derivative_derivative_U_eq_poly_in_U, Cubic.of_a_eq_zero', prod_X_sub_C_nextCoeff, leadingCoeff_quadratic, natDegree_X, idealX_span, Multiset.prod_X_sub_X_eq_sum_esymm, eraseLead_X_pow, support_C_mul_X, aroots_X_sub_C, degree_quadratic_lt, WeierstrassCurve.Affine.CoordinateRing.basis_one, cyclotomic_dvd_geom_sum_of_dvd, C_mul_X_eq_monomial, eval_det_add_X_smul, prod_multiset_X_sub_C_of_monic_of_roots_card_eq, X_mem_lifts, IsMonicOfDegree.natDegree_sub_X_pow, derivative_comp_one_sub_X, monic_X_pow_add_C, monic_multisetProd_X_sub_C, smeval_mul_X, isCoprime_of_is_root_of_eval_derivative_ne_zero, descPochhammer_succ_comp_X_sub_one, leadingCoeff_det_X_one_add_C, quotientSpanXSubCAlgEquiv_symm_apply, X_pow_sub_C_irreducible_iff_of_odd, coeff_one_add_X_pow, zero_notMem_multiset_map_X_sub_C, Irreducible.natSepDegree_eq_one_iff_of_monic', derivative_expand, X_pow_sub_C_irreducible_of_odd, StandardEtalePresentation.toPresentation_algebra_smul, sum_smul_minpolyDiv_eq_X_pow, monomial_one_one_eq_X, natDegree_mul_X, natDegree_X_pow_sub_C, Monic.natSepDegree_eq_one_iff_of_irreducible', isNilpotent_X_mul_iff, roots_C_mul_X_pow, IsDistinguishedAt.map_eq_X_pow, dickson_two_zero, LaurentPolynomial.mk'_one_X, evalβ_mul_X, iterate_derivative_eq_factorial_smul_sum, iterate_derivative_X_add_pow, Chebyshev.S_eq_U_comp_half_mul_X, evalβ_X_pow, aroots_quadratic_eq_pair_iff_of_ne_zero', derivative_X, comp_neg_X_eq_zero_iff, eq_prod_roots_of_splits, eq_prod_roots_of_monic_of_splits_id, WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_C, WeierstrassCurve.Affine.Y_sub_negPolynomial, MvPolynomial.optionEquivLeft_apply, minpoly_algHom_toLinearMap, chebyshev_U_eq_dickson_two_one, Derivation.mapCoeffs_X, Lagrange.interpolate_eq_nodalWeight_mul_nodal_div_X_sub_C, Chebyshev.C_one, LinearMap.charpoly_nilpotent_tfae, WeierstrassCurve.Affine.CoordinateRing.coe_basis, natSepDegree_X_sub_C_pow, isMonicOfDegree_two_iff', aroots_X, Multiset.prod_X_add_C_coeff, Monic.eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one, eraseLead_add_C_mul_X_pow, minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C, isMonicOfDegree_X_sub_one, degreeLT.basis_val, toContinuousMapOn_X_eq_restrict_id, reverse_mul_X_pow, ConjRootClass.minpoly.map_eq_prod, Chebyshev.S_add_one, matPolyEquiv_diagonal_X, coeff_divByMonic_X_sub_C_rec, gal_X_pow_isSolvable, Subfield.splits_bot, monic_X_pow_add, degree_lt_degree_mul_X, leadingCoeff_X_pow_add_C, smeval_X_pow, Matrix.charmatrix_apply_eq, Lagrange.nodal_insert_eq_nodal, mapAlgHom_eq_evalβAlgHom'_CAlgHom, Matrix.charpoly_natCast, coeff_mul_X_zero, eval_divByMonic_eq_trailingCoeff_comp, X_pow_eq_monomial, X_pow_sub_C_irreducible_iff_forall_prime_of_odd, toAddCircle_X_pow_eq_fourier, descPochhammer_one, as_sum_range_C_mul_X_pow', Matrix.derivative_det_one_add_X_smul, rootMultiplicity_X_sub_C_pow, resultant_X_sub_C_right, iterate_derivative_mul_X, Chebyshev.S_eq_X_mul_S_add_C, update_eq_add_sub_coeff, monic_finprod_X_sub_C, Real.Polynomial.isRoot_cos_pi_div_five, Chebyshev.S_comp_two_mul_X, WeierstrassCurve.Affine.C_addPolynomial, natDegree_finset_prod_X_sub_C_eq_card, support_C_mul_X', prod_cyclotomic_eq_X_pow_sub_one, iterate_derivative_X, Matrix.charpoly_mul_comm_of_le, Module.AEval'.X_smul_of, pow_rootMultiplicity_not_dvd, divByMonic_add_X_sub_C_mul_derivative_divByMonic_eq_derivative, aeval_X_pow, Chebyshev.S_eq, coeff_mul_X_pow, resultant_X_pow_right, Bivariate.swap_apply, eval_X, dvd_comp_X_add_C_iff, separable_X_pow_sub_C, X_comp, Monic.eq_X_pow_iff_natDegree_le_natTrailingDegree, dvd_comp_C_mul_X_add_C_iff, X_pow_smul_rTensor_monomial, X_pow_sub_one_splits, isMonicOfDegree_add_add_two, degree_X_pow_add_C, Matrix.det_one_add_smul, Monic.comp_X_sub_C, degree_X_sub_C, iterate_derivative_X_sub_pow, support_trinomial', isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top, PowerSeries.IsWeierstrassFactorization.isWeierstrassDivision, expand_eq_comp_X_pow, exists_finset_of_splits, Chebyshev.T_two, ascPochhammer_succ_comp_X_add_one, supNorm_X, Matrix.charpoly_of_upperTriangular, Chebyshev.T_add_one, gal_X_pow_sub_C_isSolvable, Lagrange.interpolate_eq_sum, coeff_X_pow_mul, FiniteField.roots_X_pow_card_sub_X, X_mul_C, coeff_C_mul_X, leadingCoeff_cubic, eval_X_pow, natDegree_eq_one, Chebyshev.C_eq_S_sub_X_mul_S, minpoly.sub_algebraMap, WeierstrassCurve.Ο_three, X_pow_mul_assoc, degreeLT.addLinearEquiv_apply_fst, coeff_X_pow, derivative_X_sub_C_sq, Matrix.charpoly_sub_scalar, MvPolynomial.optionEquivRight_X_none, aeval_X_left_apply, FiniteField.instIsSplittingFieldExtensionHSubPolynomialHPowNatXCard, cyclotomic_two, Chebyshev.U_two, degree_C_lt_degree_C_mul_X, Splits.X_pow, roots_X_pow_char_pow_sub_C_pow, isRegular_X, Multiset.prod_X_sub_C_dvd_iff_le_roots, Module.AEval'.of_symm_X_smul, sum_X_index, Matrix.IsHermitian.charpoly_cfc_eq, mem_span_C_X_sub_C_X_sub_C_iff_eval_eval_eq_zero, Chebyshev.U_eq, Chebyshev.S_sq_add_S_sq, nextCoeff_C_mul_X_add_C, X_pow_sub_one_dvd_prod_cyclotomic, prod_multiset_root_eq_finset_root, iterate_derivative_derivative_mul_X_sq, X_pow_sub_C_separable_iff, aeval_homogenize_X_one, IsPurelyInseparable.minpoly_eq, coeff_X_sub_C_mul, Cubic.of_a_eq_zero, comp_C_mul_X_eq_zero_iff, degree_quadratic, evalEval_X, monic_X_pow_sub_C, leadingCoeff_linear, rootMultiplicity_eq_natFind_of_ne_zero, isMonicOfDegree_two_iff, ascPochhammer_mul, C_mul_X_pow_eq_monomial, nextCoeff_X_add_C, StandardEtalePair.equivMvPolynomialQuotient_symm_apply, eq_X_add_C_of_degree_le_one, cyclotomic'_one, isUnit_iff', logMahlerMeasure_X_sub_C, MvPolynomial.optionEquivLeft_X_none, trailingDegree_C_mul_X_pow, Monic.quotient_isIntegralElem, X_pow_sub_one_eq_prod, prod_multiset_X_sub_C_dvd, degree_cubic_lt, AdjoinRoot.mul_div_root_cancel, eq_X_add_C_of_natDegree_le_one, minpoly.natSepDegree_eq_one_iff_eq_X_sub_C_pow, Cubic.of_b_eq_zero, natTrailingDegree_mul_X_pow, derivative_X_add_C, hermite_succ, descPochhammer_succ_right, Chebyshev.U_sub_one, Real.fibRec_charPoly_eq, Matrix.charpoly_zero, hermite_eq_iterate, WeierstrassCurve.Affine.CoordinateRing.C_addPolynomial, support_binomial', cyclotomic_eq_prod_X_sub_primitiveRoots, X_add_C_scaleRoots, Splits.comp_X_sub_C, aevalTower_X, transcendental_X, natDegree_C_mul_X, coeff_mul_X_sub_C, gal_X_pow_sub_one_isSolvable, natDegree_X_add_C, aeval_X_left, Chebyshev.U_one, degreeLT.addLinearEquiv_apply_snd, natSepDegree_C_mul_X_sub_C_pow, X_sub_C_mul_divByMonic_eq_sub_modByMonic, IsNilpotent.charpoly_eq_X_pow_finrank, roots_C_mul_X_sub_C_of_IsUnit, PowerSeries.trunc_X_of, derivative_X_pow_succ, degree_X_pow_le, bernsteinPolynomial.flip', natSepDegree_X, monic_X_add_C, logMahlerMeasure_X_add_C, toContinuousMap_X_eq_id, WeierstrassCurve.Affine.addPolynomial_slope, rootMultiplicity_eq_nat_find_of_nonzero, roots_quadratic_eq_pair_iff_of_ne_zero, derivative_X_sub_C_pow, IsMonicOfDegree.exists_natDegree_lt, eraseLead_C_mul_X, ker_constantCoeff, X_pow_sub_C_irreducible_iff_of_prime_pow, Lagrange.basis_eq_prod_sub_inv_mul_nodal_div, IsAdjoinRoot.map_X, Monic.eq_X_pow_iff_natTrailingDegree_eq_natDegree, polynomialFunctions.starClosure_eq_adjoin_X, IsRoot.mul_div_eq, sum_C_mul_X_pow_eq, LinearMap.pow_eq_aeval_mod_charpoly, PowerSeries.normalized_count_X_eq_of_coe, Module.AEval'.X_pow_smul_of, as_sum_support_C_mul_X_pow, toFinsupp_X_pow, Chebyshev.one_sub_X_sq_mul_derivative_T_eq_poly_in_T, degree_quadratic_le, eq_quadratic_of_degree_le_two, WeierstrassCurve.Ο_one, reflect_one, content_X_mul, MulSemiringAction.charpoly_eq_prod_smul, card_support_eq, reflect_monomial, leadingCoeff_pow_X_add_C, coeff_mul_X, degree_X_le, X_pow_sub_X_sub_one_irreducible, roots_C_mul_X_add_C, LinearMap.charpoly_eq_X_pow_iff, leadingCoeff_X_pow_sub_C, LaurentPolynomial.mk'_eq, separable_X, Bivariate.equivMvPolynomial_symm_X_0, minpoly.eq_X_sub_C_of_algebraMap_inj, taylor_apply, WeierstrassCurve.Affine.C_addPolynomial_slope, iterate_derivative_comp_one_sub_X, Splits.eq_prod_roots, div_wf_lemma, eq_X_add_C_of_degree_eq_one, prod_cyclotomic'_eq_X_pow_sub_one, mahlerMeasure_C_mul_X_add_C, Splits.X, evalβ_C_X, WeierstrassCurve.Affine.CoordinateRing.norm_smul_basis, IsCyclotomicExtension.isSplittingField_X_pow_sub_one, X_mul_divX_add, card_support_binomial, separable_C_mul_X_pow_add_C_mul_X_add_C', IsPrimitiveRoot.minpoly_sub_one_eq_cyclotomic_comp, WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis, Splits.comp_X_add_C, separable_X_pow_sub_C', IsCyclotomicExtension.splits_X_pow_sub_one, opRingEquiv_op_X, coe_X, Chebyshev.S_sub_one, Splits.eq_X_sub_C_of_single_root, coeff_det_X_add_C_card, bernsteinPolynomial.flip, quotientSpanXSubCAlgEquiv_mk, map_X, cyclotomic_prime_pow_eq_geom_sum, smeval_X_pow_mul, aeval_X_left_eq_map, Lagrange.X_sub_C_dvd_nodal, smeval_X, roots_X_sub_C, mkDerivationEquiv_symm_apply, natDegree_quadratic_le, Bivariate.swap_Y, rootSet_C_mul_X_pow, monomial_mul_X, iterate_derivative_X_pow_eq_natCast_mul, le_rootMultiplicity_iff, smul_X, coeff_X_one, Cubic.of_b_eq_zero', WeierstrassCurve.Affine.derivative_addPolynomial_slope, support_C_mul_X_pow', rootMultiplicity_mul_X_sub_C_pow, RatFunc.algebraMap_X, degreeLT.addLinearEquiv_apply, support_X, reflect_one_X, card_support_eq', eval_unique, Finset.prod_X_add_C_coeff, Matrix.charpoly_one, divX_mul_X_add, Subfield.roots_X_pow_char_sub_X_bot, natSepDegree_X_pow_char_pow_sub_C, LaurentPolynomial.algebraMap_X_pow, homogenize_X_pow, Matrix.det_one_add_X_smul, FiniteField.isSplittingField_of_nat_card_eq, coeff_X_of_ne_one, Module.AEval.X_pow_smul_of, degree_X_pow_sub_C, Chebyshev.T_eq, descPochhammer_eq_ascPochhammer, leadingCoeff_X, roots_X, Irreducible.natSepDegree_eq_one_iff_of_monic, natDegree_X_pow_add_C, Chebyshev.C_eq, mahlerMeasure_X_add_C, taylor_X_pow, reverse_X_pow_mul, comp_C_mul_X_coeff, cyclotomic_prime_pow_mul_X_pow_sub_one, coeff_X_zero, resultant_X_sub_C_pow_left, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none, bernsteinPolynomial.variance, toLaurent_X_pow, derivative_C_mul_X, Bivariate.swap_X, eval_iterate_derivative_rootMultiplicity, iterate_derivative_derivative_mul_X, Chebyshev.add_one_mul_self_mul_T_eq_poly_in_T, bernsteinPolynomial.sum_smul, Splits.X_add_C, bernoulli_eq_sub_sum, descPochhammer_succ_left, logMahlerMeasure_X, natTrailingDegree_X_le, comp_neg_X_leadingCoeff_eq, degree_C_mul_X_pow_le, separable_prod_X_sub_C_iff', le_trailingDegree_C_mul_X_pow, algEquivAevalNegX_symm_apply, descPochhammer_mul, AdjoinRoot.root_isInv, FiniteField.splits_X_pow_nat_card_sub_X, eq_prod_roots_of_splits_id, natDegree_X_sub_C, Bivariate.equivMvPolynomial_symm_X_1, iterate_derivative_X_pow_eq_smul, Matrix.matPolyEquiv_charmatrix, card_support_eq_three, Chebyshev.U_eq_X_mul_U_add_T, resultant_X_sub_C_pow_right, X_sub_C_dvd_sub_C_eval, degreeLT.addLinearEquiv_apply', WeierstrassCurve.Affine.Y_sub_polynomialY, prime_X_sub_C, mul_comp_neg_X, Matrix.charmatrix_natCast, hilbertPoly_X_pow_succ, Lagrange.iterate_derivative_interpolate, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, roots_X_pow_char_sub_C_pow, RatFunc.num_X, leadingCoeff_mul_X, iterate_derivative_eq_sum, quadratic_dvd_of_aeval_eq_zero_im_ne_zero, algEquivAevalXAddC_symm_apply, nextCoeff_X_sub_C, natDegree_C_mul_X_pow, C_mul_X_pow_eq_self, leadingCoeff_X_pow, degree_X_sub_C_le, smeval_X_mul, AdjoinRoot.Minpoly.coe_toAdjoin_mk_X, degree_C_mul_X_le, mul_X_pow_comp, reverse_mul_X, cyclotomic.dvd_X_pow_sub_one, eraseLead_C_mul_X_pow, Monic.natSepDegree_eq_one_iff, X_pow_sub_C_irreducible_of_prime, roots_multiset_prod_X_sub_C, bernoulli_comp_one_add_X, X_pow_dvd_iff, Matrix.charpoly_fin_two, separable_prod_X_sub_C_iff, dickson_add_two, comp_X, exists_eq_pow_rootMultiplicity_mul_and_not_dvd, Monic.eq_X_add_C, expand_X, WeierstrassCurve.Ξ¦_ofNat, eval_C_X_evalβ_map_C_X, eraseLead_X, Chebyshev.C_sub_one, card_roots_X_pow_sub_C, reverse_X_mul, X_pow_sub_one_separable_iff, leadingCoeff_C_mul_X_pow, Differential.mapCoeffs_X, WeierstrassCurve.Ξ¦_three, not_isUnit_X_add_C, Chebyshev.U_add_two, degree_cubic, LinearMap.isNilpotent_iff_charpoly, isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow, dickson_one_one_charP, degree_X_pow, resultant_X_add_C_left, gal_X_sub_C_isSolvable, hilbertPoly_mul_one_sub_succ, Bivariate.equivMvPolynomial_X, Module.AEval.of_symm_X_smul, FiniteField.isSplittingField_of_card_eq, IsMonicOfDegree.aeval_add, cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt, natDegree_multiset_prod_X_sub_C_eq_card, dickson_one_one_zmod_p, Splits.C_mul_X_pow, exists_eq_X_add_C_of_natDegree_le_one, Matrix.charpoly_coeff_eq_prod_coeff_of_le, opRingEquiv_symm_C_mul_X_pow, WeierstrassCurve.Affine.CoordinateRing.exists_smul_basis_eq, iterate_derivative_prod_X_sub_C, commute_X, monic_geom_sum_X, signVariations_eraseLead_mul_X_sub_C, X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd, mahlerMeasure_X_sub_C, minpoly.add_algebraMap, degreeLT.addLinearEquiv_symm_apply, MulSemiringAction.charpoly_eq, isMonicOfDegree_one_iff, root_X_pow_sub_C_pow, natTrailingDegree_X, bernsteinPolynomial.sum_mul_smul, natDegree_X_pow_mul, WeierstrassCurve.Ξ¦_four, MvPolynomial.finSuccEquiv_eq, eval_mul_X_pow, Chebyshev.C_add_one, factorial_mul_shiftedLegendre_eq, Chebyshev.one_sub_X_sq_mul_derivative_derivative_T_eq_poly_in_T, natDegree_X_pow_le, aroots_quadratic_eq_pair_iff_of_ne_zero, sumIDeriv_X, coeff_X_pow_self, dvd_C_mul_X_sub_one_pow_add_one, Bivariate.equivMvPolynomial_C_X, isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C, PolyEquivTensor.toFunBilinear_apply_apply, ofMultiset_apply, Cubic.prod_X_sub_C_eq, toFinsupp_X, algHom_ext_iff, Chebyshev.T_neg_two, rootMultiplicity_eq_multiplicity, X_mul, Module.AEval.X_smul_of, multiset_prod_X_sub_C_nextCoeff, Chebyshev.S_two, Lagrange.nodal_eq_mul_nodal_erase, natDegree_X_pow, divX_C_mul_X_pow, MvPolynomial.prod_X_add_C_coeff, X_pow_mul_monomial, mem_closure_X_union_C, reverse_add_C, AlgebraicClosure.Monics.map_eq_prod, degree_X, cyclotomic_one, Chebyshev.C_neg_one, coeff_X_mul_zero, mkDerivation_X, dickson_one_one_eq_chebyshev_T, FiniteField.X_pow_card_sub_X_natDegree_eq, isRegular_X_pow, prod_cyclotomic_eq_geom_sum, derivation_ext_iff, not_isUnit_X_sub_C, FiniteField.splits_X_pow_card_sub_X, card_support_eq_two, chebyshev_T_eq_dickson_one_one, reflect_C_mul_X_pow, card_support_eq_one, PolyEquivTensor.invFun_monomial, coe_expand, aroots_C_mul_X_pow, Matrix.charpoly_sub_diagonal_degree_lt, leadingCoeff_C_mul_X, degreeLT.addLinearEquiv_symm_apply', Splits.X_sub_C, iterate_derivative_mul_X_pow, IsAdjoinRootMonic.modByMonicHom_root_pow, C_leadingCoeff_mul_prod_multiset_X_sub_C, minpoly.eq_X_sub_C', Monic.comp_X_add_C, StandardEtalePresentation.toPresentation_Ο', cyclotomic_eq_prod_X_pow_sub_one_pow_moebius, coeff_X_add_one_pow, mul_X_add_natCast_comp, eq_X_sub_C_of_splits_of_single_root, content_X, card_support_C_mul_X_pow_le_one, monomial_mul_X_pow, support_C_mul_X_pow, MvPolynomial.prod_C_add_X_eq_sum_esymm, modByMonic_X_sub_C_eq_C_eval, denomsClearable_C_mul_X_pow, binomial_eq_binomial, iterate_derivative_X_pow_eq_C_mul, Matrix.charpoly_vecMulVec, Chebyshev.T_one, derivative_X_pow, MvPolynomial.optionEquivRight_apply, MvPolynomial.finSuccEquiv_apply, X_dvd_iff, X_mul_monomial, evalβ_X, Splits.eq_prod_roots_of_monic, AdjoinRoot.mk_X, isNilpotent_C_mul_pow_X_of_isNilpotent, leadingCoeff_X_sub_C, WeierstrassCurve.Ξ¦_two, Chebyshev.C_comp_two_mul_X, KaehlerDifferential.polynomial_D_apply, evalβ_X_mul, X_pow_mem_lifts, taylor_monomial, IsPurelyInseparable.minpoly_eq_X_pow_sub_C, LinearMap.charpoly_one, natDegree_X_sub_C_le, splits_X_sub_C_mul_iff, toMvPolynomial_X, FiniteField.minpoly_frobeniusAlgHom, dickson_of_two_le, Matrix.charmatrix_one, Matrix.coeff_det_one_add_X_smul_one, Chebyshev.one_sub_X_sq_mul_iterate_derivative_T_eq_poly_in_T, Chebyshev.T_neg_one, Chebyshev.U_add_one, trinomial_def, X_sub_C_scaleRoots, polyEquivTensor_apply, X_pow_sub_X_sub_one_irreducible_rat, sum_taylor_eq, cyclotomic'_two, X_mem_nonzeroDivisors, RatFunc.liftRingHom_X, natDegree_linear_le, minpoly_algEquiv_toLinearMap, natDegree_det_X_add_C_le, eval_C_X_comp_evalβ_map_C_X, AdjoinRoot.algHom_subsingleton, mod_X_sub_C_eq_C_eval, minpoly.zero, Chebyshev.one_sub_X_sq_mul_U_eq_pol_in_T, minpoly.one, degree_comp_neg_X, geom_sum_X_comp_X_add_one_eq_sum, LinearMap.charpoly_sub_smul, minpoly.neg, natSepDegree_X_sub_C, WeierstrassCurve.Affine.CoordinateRing.coe_norm_smul_basis, aroots_X_pow, Chebyshev.T_sub_one, support_X_pow, spectralValue_X_sub_C, StandardEtalePair.aeval_X_g_mul_mk_X, roots_C_mul_X_sub_C, monomial_one_right_eq_X_pow, rootMultiplicity_le_iff, eraseLead_mul_eq_mul_eraseLead_of_nextCoeff_zero, natDegree_X_le, modByMonic_X, IsPurelyInseparable.minpoly_eq_X_sub_C_pow, X_pow_sub_C_irreducible_of_prime_pow, roots_quadratic_eq_pair_iff_of_ne_zero', PowerSeries.IsWeierstrassDivision.isWeierstrassFactorization, iterate_derivative_X_sub_pow_self, X_dvd_sub_C, degreeLT_eq_span_X_pow, eval_mul_X_sub_C, minpolyDiv_spec, isNilpotent_mul_X_iff, Monic.eq_X_pow_char_pow_sub_C_of_natSepDegree_eq_one_of_irreducible, reflect_C, IsAdjoinRootMonic.modByMonicHom_root, dvd_comp_neg_X_iff, algEquivAevalNegX_apply, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, as_sum_range_C_mul_X_pow, degree_mul_X, derivative_C_mul_X_pow, signVariations_X_sub_C_mul_eraseLead_le, support_binomial, roots_X_pow_char_sub_C, dickson_two_one_eq_chebyshev_U, natTrailingDegree_X_pow, mul_X_comp, splits_X, bernoulli_one, StandardEtalePresentation.toPresentation_val, Differential.implicitDeriv_X, Chebyshev.U_sub_two, leadingCoeff_X_pow_sub_one, Chebyshev.C_eq_two_mul_T_comp_half_mul_X, FiniteField.X_pow_card_pow_sub_X_natDegree_eq, WeierstrassCurve.Ο_four, rootMultiplicity_X_sub_C_self, splits_X_sub_C, algEquivCMulXAddC_symm_apply, Chebyshev.T_eq_half_mul_C_comp_two_mul_X, natDegree_cubic, irreducible_X, IsMonicOfDegree.aeval_sub, not_isUnit_X_pow_sub_one, toFinsupp_C_mul_X_pow, dickson_two, succ_signVariations_X_sub_C_mul_monomial, derivative_X_add_C_sq, cyclotomic_three, rootMultiplicity_X_sub_C, prime_X, Matrix.charpoly_mul_comm', IsLocalization.adjoin_inv, dvd_comp_X_sub_C_iff, pow_mul_divByMonic_rootMultiplicity_eq, Chebyshev.C_sub_two, algEquivAevalXAddC_apply, eval_mul_X, cauchyBound_X_add_C, degree_cubic_le, cyclotomic_comp_X_add_one_isEisensteinAt, leadingCoeff_X_pow_add_one, matPolyEquiv_symm_X, X_sub_C_mul_removeFactor, logMahlerMeasure_C_mul_X_add_C, not_isUnit_X, Cubic.eq_prod_three_roots, FiniteField.isSplittingField_sub, Multiset.prod_X_add_C_eq_sum_esymm, exists_prod_multiset_X_sub_C_mul, degree_linear_le, Matrix.charmatrix_apply, scaleRoots_zero, derivative_X_add_C_pow, cyclotomic_prime, mul_X_sub_intCast_comp, Chebyshev.T_sub_two, splits_iff_exists_multiset', toFinsupp_C_mul_X, Matrix.charmatrix_ofNat, minpoly.natSepDegree_eq_one_iff_eq_expand_X_sub_C, dvd_iff_isRoot, Chebyshev.T_eq_X_mul_T_sub_pol_U, Multiset.prod_X_add_C_coeff', splits_X_pow, degree_linear_lt_degree_C_mul_X_sq, LinearMap.charpoly_zero, cauchyBound_X_sub_C, splits_of_exists_multiset, rootSet_X_pow, isNilpotent_pow_X_mul_C_of_isNilpotent, prod_X_sub_C_coeff_card_pred, degree_quadratic_lt_degree_C_mul_X_cb, Chebyshev.S_add_two, coeff_C_mul_X_pow, Chebyshev.C_add_two, WeierstrassCurve.Ο_two, degree_C_mul_X, homogenize_X, MvPolynomial.finSuccEquiv_X_zero, comp_X_add_C_eq_zero_iff, resultant_X_sub_C_left, hasseDeriv_X, spectralValue_eq_zero_iff, toLaurent_X, toAddCircle_X_eq_fourier_one, LaurentPolynomial.isLocalization, coeff_mul_X_pow', Lagrange.nodal_subgroup_eq_X_pow_card_sub_one, Chebyshev.T_add_two, StandardEtalePresentation.toPresentation_relation, roots_X_pow, opRingEquiv_op_C_mul_X_pow, roots_X_add_C, hilbertPoly_mul_one_sub_pow_add, mul_star_dvd_of_aeval_eq_zero_im_ne_zero, Splits.comp_neg_X, residueFieldMapCAlgEquiv_symm_X, X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd, separable_C_mul_X_pow_add_C_mul_X_add_C, Matrix.IsHermitian.charpoly_eq, taylor_X, multiset_prod_X_sub_C_coeff_card_pred, separable_X_sub_C, finiteMultiplicity_X_sub_C, MvPolynomial.optionEquivLeft_symm_X, leadingCoeff_X_add_C, degree_sum_fin_lt, ringHom_ext'_iff, irreducible_X_sub_C, Monic.as_sum, degreeLE_eq_span_X_pow, dickson_one, Cubic.C_mul_prod_X_sub_C_eq, X_pow_comp, Chebyshev.one_sub_X_sq_mul_iterate_derivative_U_eq_poly_in_U, coeff_X, bernoulli_comp_one_sub_X, irreducible_C_mul_X_add_C, smul_X_eq_monomial, commute_X_pow, Chebyshev.C_two, resultant_X_pow_left, succ_signVariations_le_X_sub_C_mul, cauchyBound_X, cfc_eval_X, le_trailingDegree_X_pow, reverse_C_add, normUnit_X, natDegree_linear, autAdjoinRootXPowSubC_root, toLaurent_C_mul_X_pow, natDegree_X_mul, Matrix.charpoly_diagonal, degree_mul_X_pow, algHom_ext'_iff, natDegree_pow_X_add_C, Monic.natSepDegree_eq_one_iff_of_irreducible, IsUnitTrinomial.irreducible_aux1, coeff_X_mul, roots_C_mul_X_add_C_of_IsUnit, bernoulli_comp_neg_X, matPolyEquiv_eq_X_pow_sub_C, cyclotomic_eq_X_pow_sub_one_div, spectralValue_X_pow, coeff_divByMonic_X_sub_C, Matrix.derivative_det_one_add_X_smul_aux, degree_C_mul_X_pow, zero_notMem_multiset_map_X_add_C, Matrix.charpoly_ofNat, leadingCoeff_divByMonic_X_sub_C, pairwise_coprime_X_sub_C, derivative_X_sub_C, Chebyshev.T_eq_U_sub_X_mul_U, comp_neg_X_comp_neg_X, natSepDegree_X_pow, Ideal.evalβ_C_mk_eq_zero, WeierstrassCurve.Ξ¦_one, isMonicOfDegree_X_pow, minpoly.eq_X_sub_C, cyclotomic_prime_mul_X_sub_one, ascPochhammer_succ_left, Chebyshev.C_neg_two, Matrix.charmatrix_diagonal, Lagrange.nodal_erase_eq_nodal_div, monic_prod_X_sub_C, natDegree_cubic_le, adjoin_X, natDegree_quadratic, natDegree_C_mul_X_pow_le, IsTranscendenceBasis.polynomial, Chebyshev.S_one, degree_linear, derivative_apply, PowerSeries.trunc_X, aeval_X, self_sub_C_mul_X_pow, le_trailingDegree_X, isCoprime_X_sub_C_of_isUnit_sub, irreducible_X_pow_sub_C_of_root_adjoin_eq_top, isMonicOfDegree_X, neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq, content_X_pow, monic_X, opRingEquiv_symm_X, trailingDegree_X_pow, Chebyshev.S_sub_two, trailingDegree_X, galois_poly_separable, coeff_X_add_C_pow, WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_Y, degree_linear_lt, ascPochhammer_succ_right, X_eq_normalize, Chebyshev.add_one_mul_T_eq_poly_in_U, support_X_empty, coeff_det_X_add_C_zero, derivative_C_mul_X_sq, Lagrange.nodal_eq, card_support_trinomial, X_pow_sub_C_irreducible_iff_of_prime, derivativeFinsupp_X, roots_X_pow_char_pow_sub_C, evalβ_algebraMap_X, Matrix.charpoly_of_card_eq_two, eval_multiset_prod_X_sub_C_derivative, smeval_mul_X_pow, X_sub_C_pow_dvd_iff, Matrix.charmatrix_zero, isCyclic_tfae, roots_prod_X_sub_C, X_pow_mul_C, gal_X_isSolvable, Multiset.prod_X_sub_C_coeff, IsPrimitiveRoot.minpoly_dvd_x_pow_sub_one, degree_X_add_C, eval_geom_sum, isMonicOfDegree_sub_add_two, hermite_one, cyclotomic'_eq_X_pow_sub_one_div, X_pow_mul, Monic.neg_one_pow_natDegree_mul_comp_neg_X, GaloisField.splits_zmod_X_pow_sub_X, monic_X_pow_sub, Monic.eq_X_sub_C_pow_of_natSepDegree_eq_one_of_splits, Matrix.isNilpotent_charpoly_sub_pow_of_isNilpotent
|
coeff π | CompOp | 449 mathmath: units_coeff_zero_smul, coeff_update_ne, WeierstrassCurve.coeff_Ξ¨βSq, MonicDegreeEq.monic, eq_C_of_derivative_eq_zero, coeff_add_eq_left_of_lt, mem_image_comap_C_basicOpen, coeff_X_pow_mul', coeff_derivative, coeff_natTrailingDegree_eq_zero, natDegree_le_iff_coeff_eq_zero, MvPolynomial.mem_image_support_coeff_finSuccEquiv, resultant_one_right, coeff_one, mem_reesAlgebra_iff_support, WeierstrassCurve.coeff_preΞ¨', Mathlib.Tactic.ComputeDegree.coeff_intCast_ite, IsUnitTrinomial.coeff_isUnit, Matrix.coeff_charpoly_mem_ideal_pow, PowerSeries.coeff_trunc, exists_eq_supNorm, MonicDegreeEq.degree, coeff_mul_natTrailingDegree_add_natTrailingDegree, resultant_add_left_deg, Ideal.coeff_zero_mem_comap_of_root_mem_of_eval_mem, Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly, IsMonicOfDegree.coeff_eq, coeff_zero_of_isScalarTower, coeff_one_add_X_pow, coeff_map, eq_C_of_degree_eq_zero, coeff_pow_eq_ite_of_natDegree_le_of_le, nextCoeff_of_natDegree_pos, coeff_sub_eq_left_of_lt, isMonicOfDegree_iff, Cubic.coeff_eq_b, coeff_shiftedLegendre, coeff_zero_eq_eval_zero, iterate_derivative_eq_factorial_smul_sum, MvPolynomial.totalDegree_coeff_finSuccEquiv_add_le, resultant_zero_right, Multiset.prod_X_add_C_coeff, Cubic.coeff_eq_c, coeff_natDegree, coeff_hermite_succ_zero, coeff_hermite_succ_succ, coeff_taylor_natDegree, coeff_divByMonic_X_sub_C_rec, roots_degree_eq_one, coeff_natTrailingDegree_pred_eq_zero, Matrix.trace_eq_neg_charpoly_coeff, content_eq_gcd_range_of_lt, coeff_minpolyDiv_sub_pow_mem_span, coeff_mul_X_zero, minpoly.coeff_zero_eq_zero, UniversalCoprimeFactorizationRing.homEquiv_comp_snd, le_gaussNorm, as_sum_range_C_mul_X_pow', coeff_eq_zero_of_lt_natTrailingDegree, MvPolynomial.degreeOf_coeff_finSuccEquiv, natTrailingDegree_ne_zero, update_eq_add_sub_coeff, logMahlerMeasure_of_degree_eq_one, Lagrange.coeff_eq_sum, integralNormalization_coeff_natDegree, constantCoeff_apply, trinomial_trailing_coeff', coeff_mul_X_pow, coe_def, coeff_ofFinsupp, coeff_mul_ofNat, resultant_X_pow_right, ext_iff, finite_range_coeff, coeff_C_ne_zero, coeff_list_sum_map, disc_of_degree_eq_two, coeff_erase, IsAdjoinRootMonic.basis_repr, LinearMap.polyCharpoly_coeff_isHomogeneous, IsSepClosed.roots_eq_zero_iff, Submodule.IsPrincipal.contentIdeal_generator_dvd_coeff, WeierstrassCurve.coeff_preΞ¨, prod_roots_eq_coeff_zero_of_monic_of_splits, coeff_X_pow_mul, trinomial_leading_coeff', coeff_C_mul_X, Cubic.coeff_eq_zero, Chebyshev.coeff_eq_iff_of_forall_abs_le_one, coeff_X_pow, coeff_isUnit_isNilpotent_of_isUnit, isUnitTrinomial_iff, eraseLead_coeff, coeff_mapAlgHom_apply, coeff_le_of_roots_le, exists_eq_gaussNorm, matPolyEquiv_symm_apply_coeff, coeff_X_sub_C_mul, UniversalFactorizationRing.jacobian_resentation, coeff_zero_eq_zero_of_zero_isRoot, PowerBasis.leftMulMatrix, eq_X_add_C_of_degree_le_one, coeff_injective, Splits.coeff_zero_eq_prod_roots_of_monic, eq_X_add_C_of_natDegree_le_one, coeff_zero_eq_leadingCoeff_mul_prod_roots_of_splits, coeff_update_apply, IsLocalization.integerNormalization_coeff, MonicDegreeEq.freeMonic_coe, span_coeff_minpolyDiv, Cubic.coeff_eq_d, resultant_C_right, coeff_mul_X_sub_C, disc_of_degree_eq_three, exists_monic_aeval_eq_zero_forall_mem_pow_of_isIntegral, MvPolynomial.finSuccEquiv_coeff_coeff, UniversalCoprimeFactorizationRing.homEquiv_comp_fst, eq_C_of_natDegree_le_zero, Differential.coeff_mapCoeffs, coeff_C_mul, coeff_monomial_of_ne, Matrix.charpoly.univ_coeff_evalβHom, hilbertPoly_succ, constantCoeff_coe, ext_iff_natDegree_le, as_sum_support_C_mul_X_pow, eq_quadratic_of_degree_le_two, le_supNorm, divX_eq_zero_iff, MulSemiringAction.smul_coeff_charpoly, coeff_map_eq_comp, coeff_mul_X, coeff_zero_prod, coeff_mul, coeff_sub_eq_neg_right_of_lt, coeff_scaleRoots, eq_X_add_C_of_degree_eq_one, coeff_mem_coeffs, natCast_coeff_zero, eq_C_of_natDegree_eq_zero, mem_span_C_coeff, X_mul_divX_add, MonicDegreeEq.coeff_of_ge, MvPolynomial.optionEquivLeft_coeff_coeff, coeff_pow_mul_natDegree, as_sum_range, coeff_natCast_ite, coeff_det_X_add_C_card, coeff_ofSubring, coeff_minpolyDiv_mem_adjoin, nextCoeff_eq_zero, WeierstrassCurve.coeff_Ξ¦, coeff_X_one, integralNormalization_coeff_degree, ite_le_natDegree_coeff, coeff_natCast_mul, IsIntegral.coeff, Finset.prod_X_add_C_coeff, divX_mul_X_add, coeff_add_eq_right_of_lt, comp_eq_zero_iff, coeff_monomial, UniversalFactorizationRing.monicDegreeEq_coe, coeff_hermite_explicit, coeff_X_of_ne_one, MvPolynomial.support_coeff_finSuccEquiv, taylor_coeff_zero, mul_eq_sum_sum, LinearMap.polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff, isUnit_iff_coeff_isUnit_isNilpotent, coeff_hermite_self, coeff_pow_of_natDegree_le, sum_eq_of_subset, eq_C_coeff_zero_iff_natDegree_eq_zero, comp_C_mul_X_coeff, natDegree_add_coeff_mul, coeff_X_zero, coeff_reflect, coeff_add, isIntegral_coeff_of_factors, lcoeff_apply, coeff_toSubring, hasseDeriv_coeff, coeff_natTrailingDegree_eq_zero_of_trailingDegree_lt, coeff_mul_C, Matrix.coeff_charpolyRev_eq_neg_trace, coeff_natDegree_succ_eq_zero, coeff_C, cyclotomic_coeff_zero, coeff_hermite_of_even_add, resultant_succ_left_deg, coeff_monomial_zero_mul, sylvester_zero_left_deg, finset_sum_coeff, MvPolynomial.mem_support_coeff_optionEquivLeft, coeff_sum, iterate_derivative_eq_sum, PolynomialModule.smul_apply, Ideal.exists_coeff_mem_comap_sdiff_comap_of_root_mem_sdiff, prodXSubSMul.coeff, coeff_mul_monomial_zero, coeff_mem_pow_of_mem_adjoin_C_mul_X, coeff_mul_add_eq_of_natDegree_le, X_pow_dvd_iff, IsRoot.dvd_coeff_zero, MvPolynomial.totalDegree_coeff_optionEquivLeft_add_le, resultant_C_left, Monic.eq_X_add_C, eq_C_of_degree_le_zero, notMem_support_iff, resultant_zero_left, PolynomialModule.smul_single_apply, MvPolynomial.optionEquivLeft_coeff_some_coeff_none, coeff_contract, supNorm_def', IsLocalization.scaleRoots_commonDenom_mem_lifts, coeff_scaleRoots_natDegree, coeff_ofNat_succ, isEisensteinAt_iff, Cubic.equiv_symm_apply_b, coeff_monomial_same, AlgebraicClosure.toSplittingField_coeff, C_dvd_iff_dvd_coeff, Matrix.charpoly.univ_coeff_isHomogeneous, trinomial_middle_coeff, Matrix.charpoly_coeff_eq_prod_coeff_of_le, num_dvd_of_is_root, coeff_smul, coeff_C_succ, sum_sq_norm_coeff_eq_circleAverage, MonicDegreeEq.map_coe, LinearMap.det_eq_sign_charpoly_coeff, coeff_ofNat_zero, WeierstrassCurve.coeff_preΞ¨β, exists_leadingCoeff_pow_smul_mem_radical_conductor, as_sum_range', isNilpotent_iff, coeff_divModByMonicAux_mem_span_pow_mul_span, MvPolynomial.image_support_finSuccEquiv, Ideal.mem_map_C_iff, LieAlgebra.engel_isBot_of_isMin.lieCharpoly_coeff_natDegree, coeff_X_pow_self, evalβ_at_zero, lifts_iff_coeff_lifts, coeff_iterate_derivative, coeff_eq_zero_of_lt_trailingDegree, MvPolynomial.prod_X_add_C_coeff, coeff_update_same, coeff_expand_mul, coeff_mul_intCast, LinearMap.polyCharpolyAux_coeff_eval, eval_eq_sum_range', smeval_at_zero, coeff_X_mul_zero, image_comap_C_basicOpen, coeff_zero_eq_aeval_zero, trailingDegree_ne_zero, coeff_sub, coeff_zero_multiset_prod, NumberField.Embeddings.coeff_bdd_of_norm_le, fourierCoeff_toAddCircle_natCast, spectralNorm.spectralNorm_eq_norm_coeff_zero_rpow, coeff_mem_radical_span_coeff_of_dvd, resultant_add_right_deg, coeff_inv_units, taylor_coeff_one, isNilpotent_tensor_residueField_iff, mem_map_range, Cubic.equiv_symm_apply_c, coeff_minpolyDiv, coeff_X_add_one_pow, matPolyEquiv_coeff_apply, coeff_opRingEquiv, sum_def, exists_monic_aeval_eq_zero_forall_mem_pow_of_mem_map, coeff_expand, X_dvd_iff, coeff_one_reverse, coeff_restriction, degree_le_iff_coeff_zero, PolyEquivTensor.toFunLinear_mul_tmul_mul_aux_2, dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAt, content_dvd_coeff, toFinsupp_apply, integralNormalization_coeff_mul_leadingCoeff_pow, coeff_ofNat_mul, Matrix.coeff_det_one_add_X_smul_one, trailingCoeff_eq_coeff_zero, zero_isRoot_iff_coeff_zero_eq_zero, aeval_eq_sum_range, sum_over_range, MonicDegreeEq.mk_coe, coeff_list_sum, sum_fin, degree_lt_iff_coeff_zero, mahlerMeasure_of_degree_eq_one, coeff_hermite_of_odd_add, IsEisensteinAt.mem, Matrix.matrixOfPolynomials_blockTriangular, MonicDegreeEq.natDegree, coeff_toSubring', degree_le_zero_iff, coeff_eq_zero_of_natDegree_lt, integralNormalization_coeff_degree_ne, isIntegral_iff_isIntegral_coeff, Splits.coeff_zero_eq_leadingCoeff_mul_prod_roots, Monic.coeff_natDegree, Algebra.mem_ideal_map_adjoin, coeff_bdd_of_roots_le, eraseLead_coeff_natDegree, Ideal.exists_coeff_ne_zero_mem_comap_of_root_mem, coeff_zero, coeff_mul_natCast, X_dvd_sub_C, Matrix.det_matrixOfPolynomials, discr_of_degree_eq_two, coeff_neg, sum_over_range', coeff_homogenize, Derivation.mapCoeffs_apply, as_sum_range_C_mul_X_pow, mem_reesAlgebra_iff, MvPolynomial.mem_support_coeff_finSuccEquiv, exists_integer_of_is_root_of_monic, PolyEquivTensor.toFunLinear_mul_tmul_mul_aux_1, intCast_coeff_zero, sum_modByMonic_coeff, coeff_eq_esymm_roots_of_card, eval_eq_sum_range, isWeaklyEisensteinAt_iff, coeff_hermite, isGreatest_supNorm, aeval_eq_sum_range', coeff_update, erase_same, taylor_coeff, spectralValue_le_one_iff, UniversalFactorizationRing.factorβ_mul_factorβ, integralNormalization_coeff, IsAlgClosed.roots_eq_zero_iff, coeff_eq_esymm_roots_of_splits, UniversalCoprimeFactorizationRing.factorβ_mul_factorβ, Monic.not_irreducible_iff_exists_add_mul_eq_coeff, AdjoinRoot.powerBasisAux'_repr_apply_to_fun, as_sum_support, coeff_expand_mul', coeff_mirror, LinearMap.polyCharpoly_coeff_eq_zero_iff_of_basis, erase_ne, coeff_divX, coeff_inj, coeff_zero_eq_aeval_zero', coeff_hermite_of_lt, mem_coeffs_iff, evalβ_eq_sum_range, mul_coeff_zero, WeierstrassCurve.coeff_Ξ¨β, Cubic.equiv_symm_apply_d, coeff_C_zero, coeff_restriction', isUnitTrinomial_iff', ext_iff_degree_le, IsIntegral.coeff_of_isFractionRing, Multiset.prod_X_add_C_coeff', IsLocalization.integerNormalization_spec, Module.Basis.traceDual_powerBasis_eq, prod_X_sub_C_coeff_card_pred, resultant_one_left, coeff_mul_monomial, coeff_C_mul_X_pow, Cubic.equiv_symm_apply_a, isIntegral_coeff_of_dvd, coeff_zero_reverse, Chebyshev.coeff_le_of_forall_abs_le_one, coeff_bernoulli, supNorm_eq_iSup, ofFn_coeff_eq_val_of_lt, coeff_mul_X_pow', coeff_mul_mirror, MvPolynomial.coeff_eval_eq_eval_coeff, evalβ_eq_sum_range', eraseLead_coeff_of_ne, Ideal.coeff_zero_mem_comap_of_root_mem, multiset_prod_X_sub_C_coeff_card_pred, IsIntegral.coeff_of_exists_smul_mem_lifts, exists_C_coeff_notMem, IsAlmostIntegral.coeff, Monic.as_sum, matPolyEquiv_coeff_apply_aux_2, norm_coeff_le_choose_mul_mahlerMeasure, WeierstrassCurve.coeff_Ξ¨Sq, spectralValueTerms_of_lt_natDegree, coeff_X, natDegree_lt_coeff_mul, coeff_reverse, resultant_X_pow_left, coeff_monomial_succ, integralNormalization_coeff_ne_natDegree, coeff_intCast_mul, Ideal.exists_coeff_ne_zero_mem_comap_of_non_zero_divisor_root_mem, coeff_comp_degree_mul_degree, Cubic.coeff_eq_a, coeff_prod_of_natDegree_le, coeff_X_mul, coeff_divByMonic_X_sub_C, ofFn_coeff_eq_zero_of_ge, MvPolynomial.IsHomogeneous.finSuccEquiv_coeff_isHomogeneous, fourierCoeff_toAddCircle, coeff_multiset_prod_of_natDegree_le, IsWeaklyEisensteinAt.mem, coeff_one_zero, coeff_mem_contentIdeal, Matrix.eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials, coeff_mul_degree_add_degree, mul_coeff_one, content_eq_gcd_range_succ, UniversalCoprimeFactorizationRing.isCoprime_factorβ_factorβ, Matrix.charpoly.univ_coeff_card, Matrix.det_eq_sign_charpoly_coeff, coeff_coe, discr_of_degree_eq_three, Module.End.eigenspace_aeval_polynomial_degree_1, inv_eq_of_aeval_divX_ne_zero, exists_monic_aeval_eq_zero_forall_mem_of_mem_map, resultant_zero_left_deg, mem_map_rangeS, degreeLT.basis_repr, resultant_zero_right_deg, Valuation.coeff_zero_minpoly, IsEisensteinAt.notMem, coeff_preHilbertPoly_self, MvPolynomial.IsHomogeneous.coeff_isHomogeneous_of_optionEquivLeft_symm, IsEisensteinAt.coeff_mem, MvPolynomial.totalDegree_coeff_optionEquivLeft_le, coeff_monomial_mul, LinearMap.polyCharpoly_coeff_eval, coeff_X_add_C_pow, coeff_natDegree_eq_zero_of_degree_lt, coeff_list_prod_of_natDegree_le, coeff_det_X_add_C_zero, coeff_eq_zero_of_degree_lt, inv_eq_of_root_of_coeff_zero_ne_zero, LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul, coeff_zero_eq_prod_roots_of_monic_of_splits, Multiset.prod_X_sub_C_coeff, coeff_freeMonic, monomial_add_erase, MvPolynomial.coe_mapEquivMonic_comp, Mathlib.Tactic.ComputeDegree.coeff_smul
|
coeffs π | CompOp | 22 mathmath: monic_restriction, coeffs_monomial, evalβ_restriction, contentIdeal_def, restriction_one, degree_restriction, coeffs_empty_iff, restriction_zero, coeff_mem_coeffs, map_restriction, coeffs_one, coeff_restriction, coeffs_nonempty_iff, natDegree_restriction, IntermediateField.adjoin_minpoly_coeff_of_exists_primitive_element, mem_coeffs_iff, coeff_restriction', support_restriction, coeffs_zero, coeffs_ofSubring, lifts_iff_coeffs_subset_range, toSubring_one
|
commRing π | CompOp | 423 mathmath: PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_apply, Lagrange.interpolate_one, RatFunc.mk_def_of_ne, PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply, RatFunc.ofFractionRing_mk', Lagrange.interpolate_eq_of_values_eq_on, RatFunc.mk_coe_def, splits_iff_exists_multiset, RatFunc.toFractionRing_injective, one_add_X_pow_sub_X_pow, eq_cyclotomic_iff, Monic.free_quotient, StandardEtalePair.inv_aeval_X_g, Lagrange.eval_interpolate_not_at_node', Differential.implicitDeriv_C, WeierstrassCurve.Affine.CoordinateRing.smul, X_pow_sub_C_eq_prod, IsAdjoinRoot.mem_ker_map, isJacobsonRing_polynomial_iff_isJacobsonRing, isIntegral_coeff_prod, AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_symm_mk, RatFunc.num_div_dvd, KaehlerDifferential.polynomialEquiv_symm, RatFunc.liftMonoidWithZeroHom_apply_ofFractionRing_mk, finrank_quotient_span_eq_natDegree_norm, prod_X_sub_C_nextCoeff, idealX_span, Multiset.prod_X_sub_X_eq_sum_esymm, Lagrange.derivative_nodal, IsPrimitiveRoot.minpoly_dvd_pow_mod, fiberEquivQuotient_tmul, WeierstrassCurve.Affine.CoordinateRing.basis_one, sum_bernoulli, eval_det_add_X_smul, RatFunc.smul_def, prod_multiset_X_sub_C_of_monic_of_roots_card_eq, dvd_iff_content_dvd_content_and_primPart_dvd_primPart, LaurentSeries.LaurentSeriesRingEquiv_def, monic_multisetProd_X_sub_C, PolynomialModule.aeval_equivPolynomial, leadingCoeff_det_X_one_add_C, quotientSpanXSubCAlgEquiv_symm_apply, sum_smul_minpolyDiv_eq_X_pow, RatFunc.denom_mul_dvd, Ideal.quotient_map_C_eq_zero, RatFunc.map_apply_ofFractionRing_mk, PowerBasis.quotientEquivQuotientMinpolyMap_apply, RatFunc.mk_smul, Lagrange.eval_interpolate_not_at_node, eq_prod_roots_of_splits, eq_prod_roots_of_monic_of_splits_id, WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_C, KaehlerDifferential.polynomialEquiv_D, Lagrange.interpolate_eq_nodalWeight_mul_nodal_div_X_sub_C, abc, finrank_quotient_span_eq_natDegree', WeierstrassCurve.Affine.CoordinateRing.coe_basis, Lagrange.interpolate_eq_sum_interpolate_insert_sdiff, WeierstrassCurve.Affine.Point.toClass_zero, ConjRootClass.minpoly.map_eq_prod, RatFunc.liftOn_ofFractionRing_mk, exists_monic_irreducible_factor, FunctionField.ringOfIntegers.instIsIntegralClosureSubtypeMemSubalgebraPolynomial, Matrix.derivative_det_one_add_X_smul, monic_finprod_X_sub_C, natDegree_finset_prod_X_sub_C_eq_card, prod_cyclotomic_eq_X_pow_sub_one, instIsAlgebraicPolynomialOfNoZeroDivisors_1, AdjoinRoot.quotEquivQuotMap_symm_apply_mk, pow_rootMultiplicity_not_dvd, AdjoinRoot.evalEval_apply, instIsIntegralPolynomial, height_eq_height_add_one, Matrix.minpoly_dvd_charpoly, Lagrange.eq_interpolate_iff, Ideal.injective_quotient_le_comap_map, dvd_comp_X_add_C_iff, dvd_comp_C_mul_X_add_C_iff, valuation_of_mk, instIsPushoutFractionRingPolynomial_1, Matrix.det_one_add_smul, WeierstrassCurve.Affine.CoordinateRing.instIsScalarTowerPolynomial, Monic.quotient_isIntegral, IsAdjoinRootMonic.basis_repr, exists_finset_of_splits, Matrix.charpoly_of_upperTriangular, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, Lagrange.interpolate_eq_sum, KaehlerDifferential.polynomialEquiv_comp_D, PowerBasis.quotientEquivQuotientMinpolyMap_apply_mk, RatFunc.mk_eq_localization_mk, factor_dvd_of_natDegree_ne_zero, AdjoinRoot.mk_eq_mk, PowerSeries.intValuation_eq_of_coe, RatFunc.mk_def, isAlt_wronskianBilin, Multiset.prod_X_sub_C_dvd_iff_le_roots, divRadical_dvd_derivative, leadingCoeff_mul_prod_normalizedFactors, RatFunc.mk_eq_div', RatFunc.ofFractionRing_div, Matrix.IsHermitian.charpoly_cfc_eq, X_pow_sub_one_dvd_prod_cyclotomic, prod_multiset_root_eq_finset_root, dvd_C_mul, RatFunc.toFractionRing_smul, WeierstrassCurve.Affine.CoordinateRing.mk_Ο, modByMonic_eq_zero_iff_quotient_eq_zero, comap_taylorEquiv_degreeLT, FunctionField.classNumber_eq_one_iff, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply_mk, Monic.quotient_isIntegralElem, X_pow_sub_one_eq_prod, prod_multiset_X_sub_C_dvd, RatFunc.ofFractionRing_one, WeierstrassCurve.Affine.CoordinateRing.C_addPolynomial, WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_neg_mul, minpoly.IsIntegrallyClosed.isIntegral_iff_leadingCoeff_dvd, cyclotomic_eq_prod_X_sub_primitiveRoots, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_add_eq, AdjoinRoot.mk_leftInverse, finrank_quotient_span_eq_natDegree, height_map_C, modByMonicHom_apply, minpoly.dvd_iff, RatFunc.smul_eq_C_mul, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk, Differential.coeff_mapCoeffs, Lagrange.degree_interpolate_erase_lt, RatFunc.ofFractionRing_zero, hilbertPoly_succ, RatFunc.ofFractionRing_add, factor_dvd_of_degree_ne_zero, PowerSeries.normalized_count_X_eq_of_coe, RatFunc.num_dvd, MulSemiringAction.charpoly_eq_prod_smul, AdjoinRoot.mk_eq_zero, Lagrange.degree_interpolate_lt, exists_dvd_map_of_isAlgebraic, rank_polynomial_polynomial, AdjoinRoot.quotEquivQuotMap_apply, IsAdjoinRootMonic.modByMonicHom_map, Splits.eq_prod_roots, LinearMap.minpoly_dvd_charpoly, PowerSeries.IsWeierstrassDivisorAt.mod'_mk_eq_mod, FunctionField.ringOfIntegers.instIsDomainSubtypeMemSubalgebraPolynomial, prod_cyclotomic'_eq_X_pow_sub_one, not_quasiFiniteAt, KummerDedekind.emultiplicity_factors_map_eq_emultiplicity, WeierstrassCurve.Affine.CoordinateRing.norm_smul_basis, gal_prod_isSolvable, WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis, RatFunc.num_inv_dvd, coeff_det_X_add_C_card, quotientSpanXSubCAlgEquiv_mk, cyclotomic_prime_pow_eq_geom_sum, Lagrange.X_sub_C_dvd_nodal, Irreducible.exists_dvd_monic_irreducible_of_isIntegral, separable_prod, le_rootMultiplicity_iff, RatFunc.ofFractionRing_comp_algebraMap, FunctionField.ringOfIntegers.instIsIntegrallyClosedSubtypeMemSubalgebraPolynomial, minpoly.ker_aeval_eq_span_minpoly, Lagrange.eq_interpolate, IsPrimitiveRoot.minpoly_dvd_expand, minpoly.isRadical, Matrix.det_one_add_X_smul, IsPrimitiveRoot.minpoly_dvd_mod_p, RatFunc.smul_eq_C_smul, RatFunc.valuation_eq_LaurentSeries_valuation, Differential.mapCoeffs_monomial, PolynomialModule.comp_apply, Differential.mapCoeffs_C, bernsteinPolynomial.variance, RatFunc.instIsScalarTowerOfIsDomainOfPolynomial, WeierstrassCurve.Affine.CoordinateRing.map_mk, bernsteinPolynomial.sum_smul, bernoulli_eq_sub_sum, prod_mahlerMeasure_eq_mahlerMeasure_prod, separable_prod_X_sub_C_iff', LaurentSeries.coe_X_compare, RatFunc.liftRingHom_ofFractionRing_algebraMap, eq_prod_roots_of_splits_id, AdjoinRoot.modByMonicHom_mk, RatFunc.one_def, WeierstrassCurve.Affine.CoordinateRing.mk_Ο, RatFunc.div_smul, X_sub_C_dvd_sub_C_eval, Lagrange.iterate_derivative_interpolate, AlgebraicClosure.Monics.splits_finsetProd, RatFunc.inv_def, RatFunc.faithfulSMul, instIsIntegrallyClosedPolynomialOfIsDomain, quadratic_dvd_of_aeval_eq_zero_im_ne_zero, wronskianBilin_apply, Differential.deriv_aeval_eq_implicitDeriv, WeierstrassCurve.Affine.CoordinateRing.instIsDomain, RatFunc.instIsScalarTowerPolynomial, quotient_mk_comp_C_isIntegral_of_isJacobsonRing, primPart_dvd, roots_multiset_prod_X_sub_C, AdjoinRoot.powerBasisAux'_repr_symm_apply, instIsAlgebraicPolynomialOfNoZeroDivisors, RatFunc.ofFractionRing_smul, separable_prod_X_sub_C_iff, PolynomialModule.equivPolynomial_single, AdjoinRoot.quotEquivQuotMap_apply_mk, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply, WeierstrassCurve.Affine.CoordinateRing.mk_Ξ¨_sq, minpoly.dvd_map_of_isScalarTower, Splits.dvd_iff_roots_le_roots, minpoly.isIntegrallyClosed_dvd_iff, natDegree_radical_le, Algebra.Norm.Transitivity.eval_zero_comp_det, Algebra.IsUnramifiedAt.not_minpoly_sq_dvd, Differential.mapCoeffs_X, Monic.finite_quotient, RatFunc.zero_def, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_neg_mul, Bivariate.pderiv_zero_equivMvPolynomial, RatFunc.ofFractionRing_injective, natDegree_multiset_prod_X_sub_C_eq_card, AlgebraicClosure.toSplittingField_coeff, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, Matrix.charpoly_coeff_eq_prod_coeff_of_le, AdjoinRoot.Polynomial.quotQuotEquivComm_mk, WeierstrassCurve.Affine.CoordinateRing.exists_smul_basis_eq, bernsteinPolynomial.linearIndependent_aux, iterate_derivative_prod_X_sub_C, eval_det, dvd_content_iff_C_dvd, IsArtinianRing.instDecompositionMonoidPolynomial, RatFunc.ofFractionRing_sub, X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd, RatFunc.v_def, divRadical_dvd_wronskian_right, PolynomialModule.equivPolynomialSelf_apply_eq, MulSemiringAction.charpoly_eq, WeierstrassCurve.Affine.CoordinateRing.C_addPolynomial_slope, WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal', IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast, RatFunc.ofFractionRing_neg, bernsteinPolynomial.sum_mul_smul, LaurentSeries.powerSeries_ext_subring, C_mul_dvd, RatFunc.liftAlgHom_apply_ofFractionRing_mk, mem_iff_annIdealGenerator_dvd, FunctionField.ringOfIntegers.instIsDedekindDomainSubtypeMemSubalgebraPolynomialOfIsSeparableRatFunc, IsAdjoinRootMonic.map_modByMonicHom, IntermediateField.isSplittingField_iSup, dvd_C_mul_X_sub_one_pow_add_one, RatFunc.denom_div_dvd, ofMultiset_apply, RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_apply, Lagrange.degree_interpolate_le, bernoulli_def, LaurentSeries.powerSeriesRingEquiv_coe_apply, multiset_prod_X_sub_C_nextCoeff, RatFunc.instIsScalarTowerOfPolynomial, Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, IsPrimitive.dvd_primPart_iff_dvd, WeierstrassCurve.Affine.CoordinateRing.map_injective, Ideal.polynomialQuotientEquivQuotientPolynomial_symm_mk, IsDistinguishedAt.algEquivQuotient_symm_apply, AlgebraicClosure.Monics.map_eq_prod, minpoly.dvd_map_of_isScalarTower', factor_dvd_of_not_isUnit, FunctionField.ringOfIntegers.algebraMap_injective, prod_cyclotomic_eq_geom_sum, RatFunc.denom_inv_dvd, roots_prod, WeierstrassCurve.Affine.Point.toClass_some, Matrix.charpoly_sub_diagonal_degree_lt, IsAdjoinRootMonic.modByMonicHom_root_pow, C_leadingCoeff_mul_prod_multiset_X_sub_C, RatFunc.liftRingHom_apply_ofFractionRing_mk, RatFunc.num_mul_dvd, WeierstrassCurve.Affine.Point.toClass_injective, Lagrange.interpolate_eq_add_interpolate_erase, Splits.eq_prod_roots_of_monic, RatFunc.num_div_dvd', KaehlerDifferential.polynomial_D_apply, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk, Lagrange.interpolate_apply, Lagrange.interpolate_eq_iff_values_eq_on, minpoly.isIntegrallyClosed_dvd, mem_ker_modByMonic, Matrix.coeff_det_one_add_X_smul_one, RatFunc.mk_def_of_mem, resultant_prod_right, FunctionField.ringOfIntegers.instIsFractionRingSubtypeMemSubalgebraPolynomial, sum_taylor_eq, mem_normalizedFactors_iff, Differential.deriv_aeval_eq, Ideal.factors_span_eq, natDegree_det_X_add_C_le, splits_prod_iff, instIsPushoutFractionRingPolynomial, AdjoinRoot.Polynomial.quotQuotEquivComm_symm_mk_mk, LaurentSeries.valuation_compare, RatFunc.ofFractionRing_inv, WeierstrassCurve.Affine.CoordinateRing.coe_norm_smul_basis, StandardEtalePair.aeval_X_g_mul_mk_X, isIntegral_iff_isIntegral_coeff, isJacobsonRing_polynomial_of_isJacobsonRing, LaurentSeries.tendsto_valuation, WeierstrassCurve.Affine.CoordinateRing.mk_Οβ_sq, rootMultiplicity_le_iff, WeierstrassCurve.Affine.CoordinateRing.basis_zero, Lagrange.interpolate_empty, RatFunc.neg_def, Splits.dvd_of_roots_le_roots, Lagrange.eq_interpolate_of_eval_eq, IsAdjoinRootMonic.modByMonicHom_root, RatFunc.ofFractionRing_eq, dvd_comp_neg_X_iff, resultant_prod_left, RatFunc.mk_zero, AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_mk, FunctionField.ringOfIntegers.instIsNoetherianPolynomialSubtypeMemSubalgebraOfIsSeparableRatFunc, Lagrange.sum_basis, IsAdjoinRoot.map_eq_zero_iff, Algebra.Norm.Transitivity.eval_zero_det_det, AdjoinRoot.quotEquivQuotMap_symm_apply, Lagrange.eval_interpolate_at_node, Ideal.isDomain_map_C_quotient, Differential.implicitDeriv_X, minpoly.dvd, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk, Lagrange.interpolate_poly_eq_self, KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map, instIsJacobsonRing, AdjoinRoot.powerBasisAux'_repr_apply_to_fun, RatFunc.mk_one', dvd_comp_X_sub_C_iff, RatFunc.liftOn_def, PowerSeries.IsWeierstrassDivisorAt.mk_mod'_eq_self, RatFunc.isScalarTower_liftAlgebra, separable_prod', exists_prod_multiset_X_sub_C_mul, divRadical_dvd_wronskian_left, RatFunc.sub_def, WeierstrassCurve.Affine.Point.toClass_eq_zero, LaurentSeries.ratfuncAdicComplRingEquiv_apply, Monic.dvd_iff_fraction_map_dvd_fraction_map, RatFunc.div_def, dvd_iff_isRoot, RatFunc.add_def, splits_of_exists_multiset, RatFunc.denom_add_dvd, rootSet_prod, prod_X_sub_C_coeff_card_pred, bernsteinPolynomial.sum, Ideal.polynomialQuotientEquivQuotientPolynomial_map_mk, roots_multiset_prod, Ideal.quotient_mk_maps_eq, RatFunc.toFractionRingRingEquiv_symm_eq, bernsteinPolynomial.linearIndependent, mul_star_dvd_of_aeval_eq_zero_im_ne_zero, residueFieldMapCAlgEquiv_symm_X, X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd, Matrix.IsHermitian.charpoly_eq, multiset_prod_X_sub_C_coeff_card_pred, WeierstrassCurve.Affine.CoordinateRing.XYIdeal'_eq, Algebra.FormallySmooth.polynomial, RatFunc.toFractionRingRingEquiv_apply, LaurentSeries.mem_integers_of_powerSeries, IsPrimitiveRoot.minpoly_dvd_cyclotomic, exists_primitive_lcm_of_isPrimitive, instFiniteDimensionalQuotientPolynomialIdealSpanSingletonSetSmithCoeffs, RatFunc.denom_dvd, not_weaklyQuasiFiniteAt, WeierstrassCurve.Affine.CoordinateRing.map_smul, Matrix.charpoly_diagonal, ker_modByMonicHom, map_dvd_map', RatFunc.mul_def, cyclotomic_eq_X_pow_sub_one_div, Matrix.derivative_det_one_add_X_smul_aux, coe_taylorEquiv, IsAdjoinRootMonic.liftPolyβ_apply, IsDistinguishedAt.algEquivQuotient_apply, irreducible_iff_lt_natDegree_lt, monic_prod_X_sub_C, residueFieldMapCAlgEquiv_algebraMap, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of, RatFunc.toFractionRingAlgEquiv_apply, RatFunc.laurentAux_ofFractionRing_mk, IsTranscendenceBasis.polynomial, Algebra.IsAlgebraic.rank_fractionRing_polynomial, isRoot_of_isRoot_iff_dvd_derivative_mul, taylorLinearEquiv_apply_coe, WeierstrassCurve.Affine.CoordinateRing.basis_apply, WeierstrassCurve.Affine.Point.toClass_apply, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, Matrix.BlockTriangular.charpoly, IsPrimitive.dvd_iff_fraction_map_dvd_fraction_map, IsAlgClosed.dvd_iff_roots_le_roots, residueFieldMapCAlgEquiv_symm_C, Lagrange.interpolate_singleton, C_content_dvd, WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_Y, coeff_det_X_add_C_zero, Lagrange.nodal_eq, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_mul_XYIdeal, RatFunc.ofFractionRing_algebraMap, eval_multiset_prod_X_sub_C_derivative, FixedPoints.minpoly.of_evalβ, X_sub_C_pow_dvd_iff, FunctionField.ringOfIntegers.not_isField, roots_prod_X_sub_C, AdjoinRoot.evalEval_mk, map_taylorEquiv_degreeLT, Multiset.prod_X_sub_C_coeff, IsPrimitiveRoot.minpoly_dvd_x_pow_sub_one, degree_radical_le, valuation_X_eq_neg_one, cyclotomic'_eq_X_pow_sub_one_div, trdeg_of_isDomain, RatFunc.ofFractionRing_mul, isIntegral_isLocalization_polynomial_quotient, KummerDedekind.quotMapEquivQuotQuotMap_symm_apply, RatFunc.toFractionRing_eq
|
commSemiring π | CompOp | 303 mathmath: RatFunc.instFaithfulSMulPolynomialLaurentSeries, coeff_prod_mem_ideal_pow_tsub, degree_normalize, minpoly.prime_of_isIntegrallyClosed, RatFunc.mk_def_of_ne, RatFunc.ofFractionRing_mk', Derivation.apply_eval_eq, coe_normUnit_of_ne_zero, RatFunc.mk_coe_def, roots_normalize, MvPolynomial.pUnitAlgEquiv_apply, eval_multiset_prod, LaurentPolynomial.mk'_one_X_pow, RatFunc.num_div, mem_image_comap_C_basicOpen, evalβ_finset_prod, ringKrullDim_succ_le_ringKrullDim_polynomial, evalβ_multiset_prod, algebraMap_pi_eq_aeval, LaurentPolynomial.mk'_mul_T, AlgebraicGeometry.Polynomial.isOpenMap_comap_C, Differential.implicitDeriv_C, WeierstrassCurve.Affine.CoordinateRing.smul, leadingCoeff_multiset_prod', RatFunc.num_div_dvd, eval_prod, ChevalleyThm.chevalley_polynomialC, WeierstrassCurve.Affine.CoordinateRing.basis_one, eval_det_add_X_smul, instIsScalarTowerPolynomial_1, isCoprime_of_is_root_of_eval_derivative_ne_zero, leadingCoeff_det_X_one_add_C, LaurentPolynomial.mk'_one_X, RatFunc.laurent_algebraMap, degree_gcd_le_left, WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_C, MvPolynomial.optionEquivLeft_apply, prime_C_iff, Derivation.mapCoeffs_X, WeierstrassCurve.Affine.CoordinateRing.coe_basis, Multiset.prod_X_add_C_coeff, matPolyEquiv_map_smul, RatFunc.laurent_div, MvPolynomial.optionEquivRight_C, UniversalCoprimeFactorizationRing.homEquiv_comp_snd, Matrix.derivative_det_one_add_X_smul, Monic.prime_of_degree_eq_one, mem_iff_eq_smul_annIdealGenerator, RatFunc.liftMonoidWithZeroHom_apply_div', RatFunc.coe_X, RatFunc.isCoprime_num_denom, FunctionField.inftyValuation.polynomial, derivative'_apply, Bivariate.aveal_eq_map_swap, Bivariate.swap_apply, RatFunc.coe_coe, natDegree_prod', natDegree_prod, instIsPushoutFractionRingPolynomial_1, Matrix.det_one_add_smul, WeierstrassCurve.Affine.CoordinateRing.instIsScalarTowerPolynomial, LaurentSeries.inducing_coe, Submodule.IsPrincipal.contentIdeal_le_span_iff_dvd, Splits.multisetProd, LaurentSeries.continuous_coe, Monic.normalize_eq_self, RatFunc.map_apply, KaehlerDifferential.polynomialEquiv_comp_D, algebraMap_def, Derivation.mapCoeffs_C, fermatLastTheoremWith'_polynomial, RatFunc.mk_eq_mk', MvPolynomial.optionEquivRight_X_none, RatFunc.mk_def, monic_multiset_prod_of_monic, leadingCoeff_mul_prod_normalizedFactors, RatFunc.mk_eq_div', Monic.irreducible_iff_lt_natDegree_lt, aeval_homogenize_X_one, instIsPushoutPolynomial_1, RatFunc.instIsFractionRingPolynomial, MvPolynomial.optionEquivRight_symm_apply, leadingCoeff_normalize, FunctionField.algebraMap_injective, mkDerivation_one_eq_derivative', natDegree_prod_le, exists_image_comap_of_monic, RatFunc.numDenom_div, IsUnit.scaleRoots_dvd_iff, UniversalCoprimeFactorizationRing.homEquiv_comp_fst, Derivation.mapCoeffs_monomial, evalEval_multiset_prod, Differential.coeff_mapCoeffs, LaurentSeries.exists_ratFunc_val_lt, RatFunc.num_algebraMap, MvPolynomial.optionEquivRight_X_some, PowerSeries.normalized_count_X_eq_of_coe, splits_prod, isOpen_image_comap_of_monic, RatFunc.liftMonoidWithZeroHom_apply_div, RatFunc.num_dvd, AlgebraicGeometry.Polynomial.imageOfDf_eq_comap_C_compl_zeroLocus, rank_polynomial_polynomial, multiset_prod_comp, RatFunc.laurentAux_div, coeff_zero_prod, LaurentPolynomial.mk'_eq, RatFunc.mk_eq_div, evalEvalRingHom_apply, instIsScalarTowerPolynomial, KummerDedekind.emultiplicity_factors_map_eq_emultiplicity, WeierstrassCurve.Affine.CoordinateRing.norm_smul_basis, isCoprime_expand, WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis, RatFunc.liftOn_div, evalEval_prod, isOpenMap_comap_C, coeff_det_X_add_C_card, mkDerivationEquiv_symm_apply, isUnit_resultant_iff_isCoprime, RatFunc.ofFractionRing_comp_algebraMap, RatFunc.algebraMap_X, algebraMap_pi_self_eq_eval, Finset.prod_X_add_C_coeff, cyclotomic.isCoprime_rat, LaurentPolynomial.algebraMap_X_pow, prime_of_degree_eq_one, Matrix.det_one_add_X_smul, degree_multiset_prod_of_monic, minpoly.prime, RatFunc.smul_eq_C_smul, RatFunc.valuation_eq_LaurentSeries_valuation, Differential.mapCoeffs_monomial, mkDerivationEquiv_apply, RatFunc.map_apply_div, leadingCoeff_prod, LaurentPolynomial.algebraMap_eq_toLaurent, Differential.mapCoeffs_C, RatFunc.liftRingHom_apply_div', RatFunc.liftRingHom_ofFractionRing_algebraMap, RatFunc.laurentAux_algebraMap, RatFunc.algebraMap_apply_div, RatFunc.div_smul, natDegree_multiset_prod, prime_X_sub_C, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, pow_sub_dvd_iterate_derivative_pow, RatFunc.liftRingHom_apply_div, isCompact_image_comap_of_monic, RatFunc.faithfulSMul, Differential.deriv_aeval_eq_implicitDeriv, RatFunc.algebraMap_C, RatFunc.instIsScalarTowerPolynomial, map_prod, natDegree_radical_le, monic_prod_of_monic, Differential.mapCoeffs_X, RatFunc.liftAlgHom_apply_div, Bivariate.pderiv_zero_equivMvPolynomial, one_lt_rootMultiplicity_iff_isRoot_gcd, homogenize_finsetProd, natSepDegree_mul_eq_iff, RatFunc.denom_div, WeierstrassCurve.Affine.CoordinateRing.exists_smul_basis_eq, instIsPushoutPolynomial, RatFunc.intDegree_polynomial, degree_prod_le, div_eq_quo_add_rem_div, degree_prod, LaurentSeries.LaurentSeries_coe, MvPolynomial.finSuccEquiv_eq, separable_def, Monic.nextCoeff_multiset_prod, RatFunc.denom_div_dvd, RatFunc.rank_ratFunc_ratFunc, normalize_eq_self_iff_monic, MvPolynomial.prod_X_add_C_coeff, Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, derivative_prod, isLocalization, scaleRoots_dvd_iff, image_comap_C_basicOpen, mkDerivation_X, FunctionField.ringOfIntegers.algebraMap_injective, derivation_ext_iff, degree_multiset_prod_le, coeff_zero_multiset_prod, degree_prod_of_monic, Separable.isCoprime, ringKrullDim_le, mkDerivation_one_eq_derivative, algebraMap_hahnSeries_apply, cyclotomic_eq_prod_X_pow_sub_one_pow_moebius, Monic.C_dvd_iff_isUnit, MvPolynomial.prod_C_add_X_eq_sum_esymm, RatFunc.liftOn'_div, MvPolynomial.optionEquivRight_apply, MvPolynomial.finSuccEquiv_apply, RatFunc.num_div_dvd', Matrix.coeff_det_one_add_X_smul_one, RatFunc.mk_def_of_mem, algebraMap_hahnSeries_injective, derivative_prod_finset, mem_normalizedFactors_iff, LaurentSeries.valuation_coe_ratFunc, Differential.deriv_aeval_eq, Ideal.factors_span_eq, derivation_C, natDegree_det_X_add_C_le, eval_C_X_comp_evalβ_map_C_X, prod_comp, instIsPushoutFractionRingPolynomial, uniqueFactorizationMonoid, coe_normUnit, RatFunc.algebraMap_apply, instFaithfulSMulPolynomial, WeierstrassCurve.Affine.CoordinateRing.coe_norm_smul_basis, Derivation.compAEval_eq, RatFunc.mk_one, RatFunc.algebraMap_injective, WeierstrassCurve.Affine.CoordinateRing.basis_zero, LaurentSeries.coe_range_dense, RatFunc.finrank_ratFunc_ratFunc, MvPolynomial.polynomial_eval_evalβ, RatFunc.ofFractionRing_eq, PrimeSpectrum.range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk, Derivation.mapCoeffs_apply, RatFunc.denom_algebraMap, Submodule.IsPrincipal.contentIdeal_generator_dvd, RatFunc.liftRingHom_comp_algebraMap, isRoot_prod, RatFunc.num_mul_eq_mul_denom_iff, leadingCoeff_multiset_prod, Differential.implicitDeriv_X, RatFunc.liftAlgHom_apply_div', exists_irreducible_of_natDegree_ne_zero, KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map, RatFunc.liftRingHom_algebraMap, RatFunc.mk_one', prime_X, RatFunc.isScalarTower_liftAlgebra, isCoprime_map, Derivation.apply_aeval_eq', exists_irreducible_of_natDegree_pos, Multiset.prod_X_add_C_eq_sum_esymm, natDegree_multiset_prod', natDegree_prod_of_monic, splits_iff_exists_multiset', Multiset.prod_X_add_C_coeff', RatFunc.num_div_denom, natDegree_multiset_prod_le, LaurentPolynomial.isLocalization, map_multiset_prod, ringKrullDim_of_isNoetherianRing, leadingCoeff_prod', RatFunc.toFractionRingRingEquiv_symm_eq, degree_multiset_prod, RatFunc.aeval_X_left_eq_algebraMap, residueFieldMapCAlgEquiv_symm_X, PowerSeries.algebraMap_apply', RatFunc.algebraMap_monomial, RatFunc.denom_dvd, natDegree_multiset_prod_of_monic, WeierstrassCurve.Affine.CoordinateRing.map_smul, normUnit_X, matPolyEquiv_smul_one, monic_normalize, coeff_prod_of_natDegree_le, MvPolynomial.aeval_natDegree_le, Derivation.compAEval_apply, resultant_eq_zero_iff, Matrix.derivative_det_one_add_X_smul_aux, pairwise_coprime_X_sub_C, Ideal.evalβ_C_mk_eq_zero, coeff_multiset_prod_of_natDegree_le, Monic.nextCoeff_prod, UniversalCoprimeFactorizationRing.isCoprime_factorβ_factorβ, residueFieldMapCAlgEquiv_algebraMap, isCoprime_iff_aeval_ne_zero, Algebra.IsAlgebraic.rank_fractionRing_polynomial, WeierstrassCurve.Affine.CoordinateRing.basis_apply, wfDvdMonoid, Splits.prod, normalizedFactors_cyclotomic_card, RatFunc.map_apply_div_ne_zero, comap_C_surjective, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, isCoprime_X_sub_C_of_isUnit_sub, mkDerivation_apply, isCoprime_iff_aeval_ne_zero_of_isAlgClosed, WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_Y, X_eq_normalize, coeff_det_X_add_C_zero, map_normalize, RatFunc.algebraMap_comp_C, RatFunc.ofFractionRing_algebraMap, exists_irreducible_of_degree_pos, C_smul_derivation_apply, monic_finprod_of_monic, degree_radical_le, degree_gcd_le_right, Derivation.apply_aeval_eq, RatFunc.toFractionRing_eq
|
distribMulAction π | CompOp | β |
distribSMul π | CompOp | 1 mathmath: WeierstrassCurve.Affine.CoordinateRing.instIsScalarTowerPolynomial
|
erase π | CompOp | 14 mathmath: update_zero_eq_erase, coeff_erase, degree_erase_lt, ofFinsupp_erase, erase_same, erase_ne, erase_mem_lifts, support_erase, toFinsupp_erase, degree_erase_le, erase_monomial, erase_def, erase_zero, monomial_add_erase
|
inhabited π | CompOp | β |
instAdd π | CompOp | 299 mathmath: IsMonicOfDegree.add_left, isUnit_C_add_X_mul_iff, isMonicOfDegree_X_add_one, IsAdjoinRoot.repr_add_sub_repr_add_repr_mem_span, separable_X_add_C, coeff_add_eq_left_of_lt, algEquivCMulXAddC_apply, one_add_X_pow_sub_X_pow, resultant_X_add_C_right, rootMultiplicity_eq_rootMultiplicity, support_trinomial, cyclotomic_six, rootMultiplicity_eq_natTrailingDegree, derivative_mul, Chebyshev.one_sub_X_sq_mul_derivative_derivative_U_eq_poly_in_U, Cubic.of_a_eq_zero', Monic.add_of_left, opRingEquiv_op_monomial, natDegree_add_le_iff_right, leadingCoeff_quadratic, degree_quadratic_lt, eval_det_add_X_smul, WeierstrassCurve.Οβ_sq, monic_X_pow_add_C, descPochhammer_succ_comp_X_sub_one, leadingCoeff_det_X_one_add_C, coeff_one_add_X_pow, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C, iterate_derivative_X_add_pow, aroots_quadratic_eq_pair_iff_of_ne_zero', isMonicOfDegree_two_iff', leadingCoeff_opRingEquiv, Multiset.prod_X_add_C_coeff, natDegree_C_add, eraseLead_add_C_mul_X_pow, monic_X_pow_add, leadingCoeff_X_pow_add_C, degree_add_eq_right_of_degree_lt, eval_divByMonic_eq_trailingCoeff_comp, add_mod, Matrix.derivative_det_one_add_X_smul, iterate_derivative_mul_X, Chebyshev.S_eq_X_mul_S_add_C, update_eq_add_sub_coeff, WeierstrassCurve.Affine.C_addPolynomial, sumIDeriv_eq_self_add, divByMonic_add_X_sub_C_mul_derivative_divByMonic_eq_derivative, dvd_comp_X_add_C_iff, dvd_comp_C_mul_X_add_C_iff, mapEquiv_symm_apply, evalβ_list_sum, isMonicOfDegree_add_add_two, degree_X_pow_add_C, Matrix.det_one_add_smul, coeff_list_sum_map, Lagrange.basisDivisor_add_symm, support_trinomial', ascPochhammer_succ_comp_X_add_one, wronskian_add_right, leadingCoeff_cubic, natDegree_eq_one, minpoly.sub_algebraMap, Matrix.charpoly_sub_scalar, opRingEquiv_op_C, cyclotomic_two, Chebyshev.S_sq_add_S_sq, nextCoeff_C_mul_X_add_C, iterate_derivative_derivative_mul_X_sq, Cubic.of_a_eq_zero, degree_quadratic, leadingCoeff_linear, isMonicOfDegree_two_iff, ascPochhammer_mul, nextCoeff_X_add_C, eq_X_add_C_of_degree_le_one, homogenize_add, RatFunc.num_denom_add, degree_cubic_lt, eq_X_add_C_of_natDegree_le_one, Cubic.of_b_eq_zero, derivative_X_add_C, Real.fibRec_charPoly_eq, support_binomial', X_add_C_scaleRoots, natDegree_X_add_C, ofFinsupp_add, monic_X_add_C, logMahlerMeasure_X_add_C, reflect_add, roots_quadratic_eq_pair_iff_of_ne_zero, IsMonicOfDegree.exists_natDegree_lt, Chebyshev.one_sub_X_sq_mul_derivative_T_eq_poly_in_T, degree_quadratic_le, eq_quadratic_of_degree_le_two, natDegree_add_eq_left_of_degree_lt, natDegree_list_sum_le, leadingCoeff_pow_X_add_C, contract_add, roots_C_mul_X_add_C, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some, taylor_apply, map_add, rootMultiplicity_add, eq_X_add_C_of_degree_eq_one, mahlerMeasure_C_mul_X_add_C, WeierstrassCurve.Affine.CoordinateRing.norm_smul_basis, natDegree_add_eq_left_of_natDegree_lt, X_mul_divX_add, card_support_binomial, separable_C_mul_X_pow_add_C_mul_X_add_C', IsPrimitiveRoot.minpoly_sub_one_eq_cyclotomic_comp, Splits.comp_X_add_C, natDegree_add_le_of_degree_le, opRingEquiv_op_X, coeff_det_X_add_C_card, natDegree_add_eq_right_of_natDegree_lt, divX_add, natDegree_quadratic_le, natDegree_add_le_iff_left, Cubic.of_b_eq_zero', WeierstrassCurve.Affine.derivative_addPolynomial_slope, coe_add, separable_def', Finset.prod_X_add_C_coeff, divX_mul_X_add, coeff_add_eq_right_of_lt, Matrix.det_one_add_X_smul, hilbertPoly_add_left, degree_add_eq_left_of_degree_lt, leadingCoeff_add_of_degree_eq, descPochhammer_eq_ascPochhammer, eraseLead_add_of_degree_lt_right, support_add, natDegree_X_pow_add_C, mahlerMeasure_X_add_C, taylor_X_pow, Mathlib.Tactic.ComputeDegree.coeff_add_of_eq, coeff_add, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none, iterate_derivative_derivative_mul_X, Chebyshev.add_one_mul_self_mul_T_eq_poly_in_T, Splits.X_add_C, PowerSeries.IsWeierstrassDivisorAt.mod_add, eraseLead_add_of_degree_lt_left, eraseLead_add_monomial_natDegree_leadingCoeff, degree_list_sum_le_of_forall_degree_le, card_support_eq_three, Chebyshev.U_eq_X_mul_U_add_T, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, quadratic_dvd_of_aeval_eq_zero_im_ne_zero, PolyEquivTensor.invFun_add, bernoulli_comp_one_add_X, Matrix.charpoly_fin_two, resultant_add_mul_right, Monic.eq_X_add_C, degree_add_le_of_le, RatFunc.intDegree_add, add_comp, not_isUnit_X_add_C, degree_cubic, monomial_add, resultant_X_add_C_left, IsMonicOfDegree.aeval_add, cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt, exists_eq_X_add_C_of_natDegree_le_one, opRingEquiv_symm_C_mul_X_pow, opRingEquiv_symm_monomial, degreeLT.addLinearEquiv_symm_apply, isMonicOfDegree_one_iff, support_opRingEquiv, eval_listSum, aroots_quadratic_eq_pair_iff_of_ne_zero, sumIDeriv_X, dvd_C_mul_X_sub_one_pow_add_one, MvPolynomial.prod_X_add_C_coeff, sum_add_index, evalEval_add, Ideal.polynomialQuotientEquivQuotientPolynomial_symm_mk, reverse_add_C, wronskian_add_left, PowerSeries.IsWeierstrassDivisionAt.add, Monic.add_of_right, card_support_eq_two, PowerSeries.add_weierstrassMod, natDegree_add_eq_right_of_degree_lt, degreeLT.addLinearEquiv_symm_apply', Monic.comp_X_add_C, coeff_X_add_one_pow, mul_X_add_natCast_comp, MvPolynomial.prod_C_add_X_eq_sum_esymm, coeff_opRingEquiv, binomial_eq_binomial, Lagrange.interpolate_eq_add_interpolate_erase, toFinsuppIso_apply, eval_add, taylor_monomial, Matrix.coeff_det_one_add_X_smul_one, leadingCoeff_add_of_degree_lt, Chebyshev.one_sub_X_sq_mul_iterate_derivative_T_eq_poly_in_T, trinomial_def, Chebyshev.C_mul_C, cyclotomic'_two, natDegree_linear_le, coeff_list_sum, natDegree_det_X_add_C_le, modByMonic_add_div, StandardEtalePair.cond, toFinsupp_add, geom_sum_X_comp_X_add_one_eq_sum, LinearMap.charpoly_sub_smul, Chebyshev.T_mul_T, WeierstrassCurve.Affine.CoordinateRing.coe_norm_smul_basis, PowerSeries.trunc_succ, degree_add_le, roots_quadratic_eq_pair_iff_of_ne_zero', support_binomial, derivative_bernoulli_add_one, sylvesterMap_apply_coe, WeierstrassCurve.Ο_four, opRingEquiv_symm_C, resultant_add_mul_left, natDegree_cubic, derivative_X_add_C_sq, cyclotomic_three, dvd_comp_X_sub_C_iff, algEquivAevalXAddC_apply, smeval_add, toFinsuppIso_symm_apply, cauchyBound_X_add_C, degree_cubic_le, cyclotomic_comp_X_add_one_isEisensteinAt, leadingCoeff_X_pow_add_one, logMahlerMeasure_C_mul_X_add_C, Multiset.prod_X_add_C_eq_sum_esymm, degree_linear_le, derivative_X_add_C_pow, natDegree_opRingEquiv, degree_add_le_of_degree_le, splits_iff_exists_multiset', Multiset.prod_X_add_C_coeff', degree_linear_lt_degree_C_mul_X_sq, degree_quadratic_lt_degree_C_mul_X_cb, add_modByMonic, comp_X_add_C_eq_zero_iff, opRingEquiv_op_C_mul_X_pow, Ideal.polynomialQuotientEquivQuotientPolynomial_map_mk, roots_X_add_C, IsMonicOfDegree.add_right, separable_C_mul_X_pow_add_C_mul_X_add_C, taylor_X, eraseLead_add_of_natDegree_lt_left, natDegree_add_le_of_le, leadingCoeff_X_add_C, Monic.as_sum, mapEquiv_apply, Chebyshev.one_sub_X_sq_mul_iterate_derivative_U_eq_poly_in_U, irreducible_C_mul_X_add_C, reverse_C_add, degree_add_eq_of_leadingCoeff_add_ne_zero, natDegree_linear, degree_add_C, natDegree_pow_X_add_C, IsUnitTrinomial.irreducible_aux1, roots_C_mul_X_add_C_of_IsUnit, bernoulli_comp_neg_X, Matrix.derivative_det_one_add_X_smul_aux, C_add, zero_notMem_multiset_map_X_add_C, bernsteinPolynomial.derivative_succ_aux, ascPochhammer_succ_left, natDegree_cubic_le, eraseLead_add_of_natDegree_lt_right, WeierstrassCurve.Ξ¨_odd, natDegree_quadratic, aeval_add, degree_linear, natDegree_add_C, DenomsClearable.add, opRingEquiv_symm_X, degree_list_sum_le, coeff_X_add_C_pow, WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_Y, degree_linear_lt, ascPochhammer_succ_right, Chebyshev.add_one_mul_T_eq_poly_in_U, coeff_det_X_add_C_zero, card_support_trinomial, leadingCoeff_add_of_degree_lt', IsMonicOfDegree.of_dvd_sub, exists_mul_add_mul_eq_C_resultant, Matrix.charpoly_of_card_eq_two, X_sub_C_pow_dvd_iff, add_scaleRoots_of_natDegree_eq, derivative_add, degree_X_add_C, evalβ_add, monomial_add_erase, isMonicOfDegree_sub_add_two, natDegree_add_le
|
instDecidableEq π | CompOp | 14 mathmath: splits_of_splits_gcd_right, splits_of_splits_gcd_left, length_coeffList_eq_ite, PowerSeries.normalized_count_X_eq_of_coe, isRoot_gcd_iff_isRoot_left_right, cardPowDegree_apply, gcd_map, rootMultiplicity_eq_multiplicity, root_gcd_iff_root_left_right, degreeLT_eq_span_X_pow, evalβ_gcd_eq_zero, degreeLE_eq_span_X_pow, eval_gcd_eq_zero, normalizedFactors_cyclotomic_card
|
instIntCast π | CompOp | 27 mathmath: derivative_intCast_mul, Mathlib.Tactic.ComputeDegree.coeff_intCast_ite, Chebyshev.one_sub_X_sq_mul_derivative_derivative_U_eq_poly_in_U, Chebyshev.T_derivative_eq_U, evalEval_intCast, C_eq_intCast, Chebyshev.one_sub_X_sq_mul_derivative_T_eq_poly_in_T, Mathlib.Tactic.ComputeDegree.natDegree_intCast_le, intCast_comp, map_intCast, Chebyshev.add_one_mul_self_mul_T_eq_poly_in_T, degree_intCast_le, intCast_inj, eval_intCast, Chebyshev.one_sub_X_sq_mul_derivative_derivative_T_eq_poly_in_T, coeff_mul_intCast, Chebyshev.one_sub_X_sq_mul_iterate_derivative_T_eq_poly_in_T, intCast_coeff_zero, natDegree_intCast, iterate_derivative_intCast_mul, toFinsupp_intCast, Chebyshev.one_sub_X_sq_mul_iterate_derivative_U_eq_poly_in_U, coeff_intCast_mul, natTrailingDegree_intCast, ofFinsupp_intCast, Chebyshev.add_one_mul_T_eq_poly_in_U, derivative_intCast
|
instMul π | CompOp | 696 mathmath: mul_div_eq_iff_isRoot, units_coeff_zero_smul, isUnit_C_add_X_mul_iff, natDegree_mul_X_pow, natDegree_mul_leadingCoeff_inv, degreeLT.addLinearEquiv_symm_apply_inr, isLeftCancelMulZero_iff, X_pow_mul_assoc_C, leadingCoeff_mul_X_pow, degree_mul_le, mul_divByMonic_cancel_left, eq_X_sub_C_of_separable_of_root_eq, derivative_X_sq, IsWeaklyEisensteinAt.mul, smeval_monomial_mul, splits_iff_exists_multiset, Chebyshev.T_eq_X_mul_U_sub_U, IsDistinguishedAt.mul, IsSplittingField.mul, algEquivCMulXAddC_apply, mul_divByMonic_eq_iff_isRoot, RatFunc.num_div, coeff_X_pow_mul', eq_cyclotomic_iff, StandardEtalePair.inv_aeval_X_g, expand_eq_sum, AdjoinRoot.minpoly_root, derivative_intCast_mul, expNegInvGlue.hasDerivAt_polynomial_eval_inv_mul, derivative_C_mul, support_trinomial, PowerSeries.weierstrassDistinguished_mul, derivative_mul, div_def, Chebyshev.one_sub_X_sq_mul_derivative_derivative_U_eq_poly_in_U, Cubic.of_a_eq_zero', WeierstrassCurve.Ξ¨Sq_even, coeff_mul_natTrailingDegree_add_natTrailingDegree, opRingEquiv_op_monomial, Monic.leadingCoeff_C_mul, leadingCoeff_quadratic, Multiset.prod_X_sub_X_eq_sum_esymm, coeffList_C_mul, support_C_mul_X, nnqsmul_eq_C_mul, leadingCoeff_C_mul_of_isUnit, fiberEquivQuotient_tmul, taylor_mul, degree_quadratic_lt, C_mul_X_eq_monomial, logMahlerMeasure_C_mul, map_mul, WeierstrassCurve.Οβ_sq, smeval_mul_X, derivative_expand, derivative_pow_succ, StandardEtalePresentation.toPresentation_algebra_smul, RatFunc.denom_mul_dvd, natDegree_mul_X, minpoly.eq_of_irreducible, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C, isNilpotent_X_mul_iff, roots_C_mul_X_pow, evalβ_mul_X, iterate_derivative_eq_factorial_smul_sum, WeierstrassCurve.Ξ¨Sq_odd, Chebyshev.S_eq_U_comp_half_mul_X, degree_C_mul_of_isUnit, aroots_quadratic_eq_pair_iff_of_ne_zero', degree_mul_leadingCoeff_inv, eq_prod_roots_of_splits, WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_C, chebyshev_U_eq_dickson_two_one, Lagrange.interpolate_eq_nodalWeight_mul_nodal_div_X_sub_C, abc, cyclotomic_expand_eq_cyclotomic_mul, Lagrange.interpolate_eq_sum_interpolate_insert_sdiff, isMonicOfDegree_two_iff', leadingCoeff_opRingEquiv, C_mul', eraseLead_add_C_mul_X_pow, matPolyEquiv_map_smul, natDegree_mul_mirror, reverse_mul_X_pow, Chebyshev.S_add_one, Chebyshev.T_derivative_eq_U, roots_C_mul, leadingCoeff_mul, degree_list_prod, degree_lt_degree_mul_X, Lagrange.nodal_insert_eq_nodal, mapAlgHom_eq_evalβAlgHom'_CAlgHom, root_mul_right_of_isRoot, instIsRightCancelMulZeroOfIsCancelAdd, map_list_prod, coeff_mul_X_zero, natDegree_mul, monomial_mul_C, UniversalCoprimeFactorizationRing.homEquiv_comp_snd, as_sum_range_C_mul_X_pow', iterate_derivative_mul_X, Chebyshev.S_eq_X_mul_S_add_C, update_eq_add_sub_coeff, degree_C_mul_of_mul_ne_zero, Chebyshev.S_comp_two_mul_X, WeierstrassCurve.Affine.C_addPolynomial, support_C_mul_X', Mathlib.Tactic.ComputeDegree.coeff_mul_add_of_le_natDegree_of_eq_ite, degree_list_prod_le, Matrix.charpoly_mul_comm_of_le, divByMonic_add_X_sub_C_mul_derivative_divByMonic_eq_derivative, Chebyshev.S_eq, coeff_mul_X_pow, coeff_mul_ofNat, WeierstrassCurve.preΞ¨_odd, logMahlerMeasure_mul_eq_add_logMahelerMeasure, dvd_comp_C_mul_X_add_C_iff, mapEquiv_symm_apply, isRightCancelMulZero_iff, isMonicOfDegree_add_add_two, evalβ_mul', support_trinomial', exists_finset_of_splits, Chebyshev.T_two, WeierstrassCurve.Ξ¨Sq_ofNat, Chebyshev.T_add_one, irreducible_mul_leadingCoeff_inv, evalβ_list_prod, natCast_mul, Lagrange.interpolate_eq_sum, logMahlerMeasure_mul_eq_add_logMahlerMeasure, coeff_X_pow_mul, X_mul_C, coeff_C_mul_X, leadingCoeff_cubic, natDegree_eq_one, isCancelMulZero_iff, Chebyshev.C_eq_S_sub_X_mul_S, WeierstrassCurve.Ο_three, X_pow_mul_assoc, rootMultiplicity_mul, derivative_X_sub_C_sq, smul_eq_C_mul, opRingEquiv_op_C, Chebyshev.U_two, degree_C_lt_degree_C_mul_X, aroots_C_mul, isRegular_X, leadingCoeff_mul_prod_normalizedFactors, Separable.unit_mul, Chebyshev.U_eq, Separable.mul_unit, Chebyshev.S_sq_add_S_sq, nextCoeff_C_mul_X_add_C, dvd_C_mul, iterate_derivative_derivative_mul_X_sq, reverse_mul_of_domain, nextCoeff_mul_C, coeff_X_sub_C_mul, Cubic.of_a_eq_zero, comp_C_mul_X_eq_zero_iff, degree_quadratic, leadingCoeff_linear, isMonicOfDegree_two_iff, ascPochhammer_mul, C_mul_X_pow_eq_monomial, StandardEtalePair.equivMvPolynomialQuotient_symm_apply, PowerSeries.trunc_mul_C, eq_X_add_C_of_degree_le_one, WeierstrassCurve.preΞ¨'_even, RatFunc.num_denom_add, IsPrimitive.mul, natDegree_mul_leadingCoeff_self_inv, trailingDegree_C_mul_X_pow, degree_cubic_lt, AdjoinRoot.mul_div_root_cancel, eq_X_add_C_of_natDegree_le_one, Cubic.of_b_eq_zero, natTrailingDegree_mul_X_pow, hermite_succ, descPochhammer_succ_right, Chebyshev.U_sub_one, mul_scaleRoots_of_noZeroDivisors, PolyEquivTensor.toFunLinear_mul_tmul_mul, hermite_eq_iterate, WeierstrassCurve.Affine.CoordinateRing.C_addPolynomial, support_binomial', iterate_derivative_natCast_mul, WeierstrassCurve.Ξ¨_ofNat, natDegree_C_mul_X, degree_mul_le_of_le, coeff_mul_X_sub_C, RatFunc.numDenom_div, UniversalCoprimeFactorizationRing.homEquiv_comp_fst, Chebyshev.U_one, natSepDegree_C_mul_X_sub_C_pow, X_sub_C_mul_divByMonic_eq_sub_modByMonic, roots_C_mul_X_sub_C_of_IsUnit, derivative_X_pow_succ, WeierstrassCurve.Affine.addPolynomial_slope, coeff_C_mul, roots_quadratic_eq_pair_iff_of_ne_zero, derivative_X_sub_C_pow, natDegree_C_mul_eq_of_mul_eq_one, list_prod_comp, eraseLead_C_mul_X, Matrix.charpoly_fromBlocks_zeroββ, Lagrange.basis_eq_prod_sub_inv_mul_nodal_div, IsRoot.mul_div_eq, sum_C_mul_X_pow_eq, natTrailingDegree_mul_mirror, as_sum_support_C_mul_X_pow, Chebyshev.one_sub_X_sq_mul_derivative_T_eq_poly_in_T, degree_quadratic_le, eq_quadratic_of_degree_le_two, content_X_mul, card_support_eq, coeff_mul_X, coeff_mul, roots_C_mul_X_add_C, natDegree_C_mul_le, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some, noZeroDivisors_iff, natDegree_C_mul_of_mul_ne_zero, WeierstrassCurve.Affine.C_addPolynomial_slope, natDegree_mul', iterate_derivative_comp_one_sub_X, Splits.eq_prod_roots, div_wf_lemma, derivative_natCast_mul, eq_X_add_C_of_degree_eq_one, sup_ker_aeval_eq_ker_aeval_mul_of_coprime, mahlerMeasure_C_mul_X_add_C, smeval_mul, WeierstrassCurve.Affine.CoordinateRing.norm_smul_basis, X_mul_divX_add, card_support_binomial, separable_C_mul_X_pow_add_C_mul_X_add_C', C_mul_monomial, monic_C_mul_of_mul_leadingCoeff_eq_one, opRingEquiv_op_X, natDegree_mul_C_eq_of_mul_eq_one, Chebyshev.S_sub_one, content_C_mul, Splits.eq_X_sub_C_of_single_root, modByMonic_eq_sub_mul_div, Monic.nextCoeff_mul, smeval_X_pow_mul, eval_mul, Monic.isRegular, IsMonicOfDegree.mul, eval_list_prod, WeierstrassCurve.C_Ξ¨βSq, natDegree_quadratic_le, rootSet_C_mul_X_pow, monomial_mul_X, iterate_derivative_X_pow_eq_natCast_mul, Cubic.of_b_eq_zero', WeierstrassCurve.Affine.derivative_addPolynomial_slope, support_C_mul_X_pow', eq_C_content_mul_primPart, rootMultiplicity_mul_X_sub_C_pow, card_support_eq', coeff_natCast_mul, separable_def', divX_mul_X_add, card_support_mul_le, le_trailingDegree_mul, RatFunc.num_denom_mul, Matrix.det_one_add_X_smul, resultant_mul_left, Chebyshev.T_eq, content_mul_aux, mul_eq_sum_sum, divX_C_mul, Chebyshev.C_eq, degree_mul_leadingCoeff_self_inv, WeierstrassCurve.Ο_even, reverse_X_pow_mul, degree_le_mul_left, mahlerMeasure_mul, comp_C_mul_X_coeff, cyclotomic_prime_pow_mul_X_pow_sub_one, natDegree_add_coeff_mul, evalRingHom_mapMatrix_comp_compRingEquiv, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none, bernsteinPolynomial.variance, derivative_C_mul_X, iterate_derivative_derivative_mul_X, Chebyshev.add_one_mul_self_mul_T_eq_poly_in_T, descPochhammer_succ_left, degree_C_mul_X_pow_le, le_trailingDegree_C_mul_X_pow, Monic.mul_right_eq_zero_iff, descPochhammer_mul, AdjoinRoot.root_isInv, hasseDeriv_mul, self_mul_modByMonic, coeff_mul_C, eq_prod_roots_of_splits_id, natDegree_C_mul, card_support_eq_three, Chebyshev.U_eq_X_mul_U_add_T, aeval_mul, smeval_C_mul, mul_comp_neg_X, coeff_monomial_zero_mul, Lagrange.iterate_derivative_interpolate, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, splits_mul_iff, leadingCoeff_mul_X, iterate_derivative_eq_sum, quadratic_dvd_of_aeval_eq_zero_im_ne_zero, natDegree_C_mul_X_pow, dvd_mul_leadingCoeff_inv, C_mul_X_pow_eq_self, instIsCancelMulZeroOfIsCancelAdd, smeval_X_mul, mirror_mul_of_domain, degree_C_mul_X_le, mul_X_pow_comp, coeff_mul_monomial_zero, reverse_mul_X, mul_self_modByMonic, eraseLead_C_mul_X_pow, coeff_mul_add_eq_of_natDegree_le, homogenize_C_mul, Matrix.charpoly_fin_two, evalβ_mul_C', resultant_add_mul_right, natDegree_mul_C_of_isUnit, dickson_add_two, exists_eq_pow_rootMultiplicity_mul_and_not_dvd, derivative_comp, IsMonicOfDegree.eq_isMonicOfDegree_one_or_two_mul, WeierstrassCurve.Ξ¦_ofNat, toFinsupp_mul, degree_mul', Chebyshev.C_sub_one, evalβ_mul, RatFunc.intDegree_add, reverse_X_mul, mul_scaleRoots, derivative_sq, leadingCoeff_C_mul_X_pow, WeierstrassCurve.Ξ¦_three, Chebyshev.U_add_two, degree_cubic, natSepDegree_C_mul, WeierstrassCurve.preΞ¨'_odd, hilbertPoly_mul_one_sub_succ, Gal.mul_splits_in_splittingField_of_mul, natSepDegree_mul_eq_iff, Splits.C_mul_X_pow, exists_eq_X_add_C_of_natDegree_le_one, RatFunc.denom_div, opRingEquiv_symm_C_mul_X_pow, iterate_derivative_prod_X_sub_C, commute_X, signVariations_eraseLead_mul_X_sub_C, opRingEquiv_symm_monomial, X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd, reflect_mul, degreeLT.addLinearEquiv_symm_apply, WeierstrassCurve.Ο_odd, WeierstrassCurve.Ξ¨_even, support_opRingEquiv, natDegree_X_pow_mul, WeierstrassCurve.Ξ¦_four, C_mul_dvd, eval_mul_X_pow, Chebyshev.C_add_one, factorial_mul_shiftedLegendre_eq, Chebyshev.one_sub_X_sq_mul_derivative_derivative_T_eq_poly_in_T, div_C, aroots_quadratic_eq_pair_iff_of_ne_zero, dvd_C_mul_X_sub_one_pow_add_one, natDegree_mul_C_eq_of_mul_ne_zero, Cubic.prod_X_sub_C_eq, Chebyshev.T_neg_two, X_mul, derivative_evalβ_C, splits_of_splits_mul, eval_natCast_mul, Lagrange.nodal_eq_mul_nodal_erase, divX_C_mul_X_pow, X_pow_mul_monomial, Ideal.polynomialQuotientEquivQuotientPolynomial_symm_mk, coeff_mul_intCast, derivative_pow, reverse_add_C, derivative_prod, coeff_X_mul_zero, leadingCoeff_monic_mul, dickson_one_one_eq_chebyshev_T, leadingCoeff_mul_C_of_isUnit, isRegular_X_pow, card_support_eq_two, eq_mul_leadingCoeff_of_monic_of_dvd_of_natDegree_le, Matrix.charpoly_fromBlocks_zeroββ, chebyshev_T_eq_dickson_one_one, iterate_derivative_C_mul, reflect_C_mul_X_pow, card_support_eq_one, Monic.degree_mul, roots_mul, aroots_C_mul_X_pow, leadingCoeff_C_mul_X, degreeLT.addLinearEquiv_symm_apply', coe_mul, iterate_derivative_mul_X_pow, C_leadingCoeff_mul_prod_multiset_X_sub_C, RatFunc.mk_eq_mk, sup_ker_aeval_le_ker_aeval_mul, splits_mul, reverse_mul, RatFunc.num_mul_dvd, StandardEtalePresentation.toPresentation_Ο', roots_list_prod, monic_mul_C_of_leadingCoeff_mul_eq_one, IsIntegrallyClosed.eq_map_mul_C_of_dvd, mul_X_add_natCast_comp, monic_mul_leadingCoeff_inv, eq_X_sub_C_of_splits_of_single_root, card_support_C_mul_X_pow_le_one, monomial_mul_X_pow, support_C_mul_X_pow, MvPolynomial.prod_C_add_X_eq_sum_esymm, denomsClearable_C_mul_X_pow, coeff_opRingEquiv, binomial_eq_binomial, iterate_derivative_X_pow_eq_C_mul, instIsLeftCancelMulZeroOfIsCancelAdd, derivative_X_pow, leadingCoeff_mul', degree_C_mul, X_mul_monomial, Lagrange.interpolate_eq_add_interpolate_erase, mul_mod, toFinsuppIso_apply, isNilpotent_C_mul_pow_X_of_isNilpotent, RatFunc.num_div_dvd', WeierstrassCurve.Ξ¦_two, IsMonicOfDegree.eq_isMonicOfDegree_two_mul_isMonicOfDegree, Chebyshev.C_comp_two_mul_X, PolyEquivTensor.toFunLinear_mul_tmul_mul_aux_2, instNoZeroDivisors, evalβ_X_mul, taylor_monomial, Lagrange.interpolate_apply, C_mul, splits_X_sub_C_mul_iff, coeff_ofNat_mul, RatFunc.natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree, dickson_of_two_le, Chebyshev.one_sub_X_sq_mul_iterate_derivative_T_eq_poly_in_T, Chebyshev.U_add_one, trinomial_def, Chebyshev.C_mul_C, sum_taylor_eq, derivative_prod_finset, gal_mul_isSolvable, IsMonicOfDegree.eq_isMonicOfDegree_one_mul_isMonicOfDegree, natDegree_linear_le, root_mul_left_of_isRoot, modByMonic_add_div, AdjoinRoot.algHom_subsingleton, StandardEtalePair.cond, Chebyshev.one_sub_X_sq_mul_U_eq_pol_in_T, root_mul, geom_sum_X_comp_X_add_one_eq_sum, LinearMap.charpoly_prodMap, minpoly.neg, Chebyshev.T_mul_T, WeierstrassCurve.Affine.CoordinateRing.coe_norm_smul_basis, Chebyshev.T_sub_one, StandardEtalePair.aeval_X_g_mul_mk_X, roots_C_mul_X_sub_C, evalβ_mul_eq_zero_of_right, ofFinsupp_mul, eraseLead_mul_eq_mul_eraseLead_of_nextCoeff_zero, integralNormalization_mul_C_leadingCoeff, bernsteinPolynomial.derivative_succ, roots_quadratic_eq_pair_iff_of_ne_zero', coeff_mul_natCast, eval_mul_X_sub_C, minpolyDiv_spec, isNilpotent_mul_X_iff, Splits.C_mul, reflect_C, reflect_C_mul, Matrix.charpoly_inv, leadingCoeff_mul_monic, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, as_sum_range_C_mul_X_pow, content_mul, degree_mul_X, derivative_C_mul_X_pow, signVariations_X_sub_C_mul_eraseLead_le, support_binomial, degree_mul_C_of_isUnit, AdjoinRoot.minpoly_powerBasis_gen, derivative_bernoulli_add_one, dickson_two_one_eq_chebyshev_U, C_mul_comp, mul_X_comp, RatFunc.num_mul_eq_mul_denom_iff, StandardEtalePresentation.toPresentation_val, sylvesterMap_apply_coe, natDegree_mul_C_le, natTrailingDegree_mul, contentIdeal_mul_eq_top_of_contentIdeal_eq_top, Chebyshev.U_sub_two, Monic.natDegree_mul, Chebyshev.C_eq_two_mul_T_comp_half_mul_X, natDegree_mul_C, rootMultiplicity_mul', WeierstrassCurve.Ο_four, natDegree_mul_le_of_le, algEquivCMulXAddC_symm_apply, Chebyshev.T_eq_half_mul_C_comp_two_mul_X, opRingEquiv_symm_C, UniversalFactorizationRing.factorβ_mul_factorβ, resultant_add_mul_left, natDegree_cubic, UniversalCoprimeFactorizationRing.factorβ_mul_factorβ, toFinsupp_C_mul_X_pow, mul_comp, natDegree_C_mul_of_isUnit, dickson_two, succ_signVariations_X_sub_C_mul_monomial, derivative_X_add_C_sq, natSepDegree_mul_of_isCoprime, comp_eq_sum_left, Monic.mul_natDegree_lt_iff, Monic.natDegree_mul_comm, Matrix.charpoly_mul_comm', IsLocalization.adjoin_inv, Monic.mul_left_eq_zero_iff, aroots_mul, MvPolynomial.universalFactorizationMap_freeMonic, natDegree_mul_le, pow_mul_divByMonic_rootMultiplicity_eq, Chebyshev.C_sub_two, contract_mul_expand, eval_mul_X, toFinsuppIso_symm_apply, degree_cubic_le, WeierstrassCurve.Ξ¨_four, mul_coeff_zero, evalEval_list_prod, toLaurent_C_mul_eq, X_sub_C_mul_removeFactor, logMahlerMeasure_C_mul_X_add_C, Cubic.eq_prod_three_roots, Multiset.prod_X_add_C_eq_sum_esymm, exists_prod_multiset_X_sub_C_mul, degree_linear_le, derivative_X_add_C_pow, natDegree_opRingEquiv, mul_X_sub_intCast_comp, resultant_mul_right, Chebyshev.T_sub_two, splits_iff_exists_multiset', toFinsupp_C_mul_X, isUnitTrinomial_iff', iterate_derivative_mul, Chebyshev.T_eq_X_mul_T_sub_pol_U, qsmul_eq_C_mul, Gal.restrictProd_injective, degree_linear_lt_degree_C_mul_X_sq, splits_of_exists_multiset, RatFunc.denom_add_dvd, iterate_derivative_intCast_mul, isNilpotent_pow_X_mul_C_of_isNilpotent, coeff_mul_monomial, degree_quadratic_lt_degree_C_mul_X_cb, Chebyshev.S_add_two, coeff_C_mul_X_pow, Chebyshev.C_add_two, WeierstrassCurve.Ο_two, evalβ_mul_eq_zero_of_left, degree_C_mul_X, PowerSeries.IsWeierstrassFactorizationAt.mul, derivative_bernoulli, natSepDegree_mul, coeff_mul_X_pow', coeff_mul_mirror, degree_mul_C, div_C_mul, resultant_C_mul_left, Chebyshev.T_add_two, StandardEtalePresentation.toPresentation_relation, opRingEquiv_op_C_mul_X_pow, Ideal.polynomialQuotientEquivQuotientPolynomial_map_mk, contentIdeal_mul_le_mul_contentIdeal, WeierstrassCurve.Ξ¨Sq_four, natCast_mul_comp, hilbertPoly_mul_one_sub_pow_add, mul_star_dvd_of_aeval_eq_zero_im_ne_zero, bernsteinPolynomial.derivative_zero, splits_of_splits_mul', base_mul_mem_lifts, le_rootMultiplicity_mul, X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd, separable_C_mul_X_pow_add_C_mul_X_add_C, degree_sum_fin_lt, Monic.mul, Monic.as_sum, trailingDegree_mul', mapEquiv_apply, Cubic.C_mul_prod_X_sub_C_eq, eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le, Chebyshev.one_sub_X_sq_mul_iterate_derivative_U_eq_poly_in_U, bernoulli_comp_one_sub_X, natDegree_lt_coeff_mul, isUnit_leadingCoeff_mul_right_eq_zero_iff, irreducible_C_mul_X_add_C, commute_X_pow, succ_signVariations_le_X_sub_C_mul, IsMonicOfDegree.of_dvd_add, reverse_C_add, natDegree_linear, toLaurent_C_mul_X_pow, isUnit_leadingCoeff_mul_left_eq_zero_iff, coeff_intCast_mul, natDegree_X_mul, Splits.mul, degree_mul_X_pow, le_natTrailingDegree_mul, IsUnitTrinomial.irreducible_aux1, coeff_X_mul, roots_C_mul_X_add_C_of_IsUnit, mul_modByMonic, degree_C_mul_X_pow, mod_def, Separable.mul, Monic.degree_mul_comm, primPart_mul, bernsteinPolynomial.derivative_succ_aux, mul_contentIdeal_le_radical_contentIdeal_mul, Chebyshev.T_eq_U_sub_X_mul_U, cyclotomic_prime_mul_X_sub_one, ascPochhammer_succ_left, natDegree_cubic_le, coeff_mul_degree_add_degree, mul_coeff_one, WeierstrassCurve.Ο_four, WeierstrassCurve.Ξ¨_odd, natDegree_quadratic, natDegree_C_mul_X_pow_le, mul_scaleRoots', isRoot_of_isRoot_iff_dvd_derivative_mul, resultant_C_mul_right, homogenize_mul, degree_linear, evalβ_list_prod_noncomm, derivative_apply, nextCoeff_C_mul, self_sub_C_mul_X_pow, monomial_comp, eval_C_mul, natTrailingDegree_mul', neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq, monomial_mul_monomial, signVariations_C_mul, opRingEquiv_symm_X, coeff_monomial_mul, reflect_mul_induction, Chebyshev.S_sub_two, WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_Y, degree_linear_lt, WeierstrassCurve.preΞ¨_even, coeff_list_prod_of_natDegree_le, ascPochhammer_succ_right, PowerSeries.trunc_C_mul, Chebyshev.add_one_mul_T_eq_poly_in_U, evalEval_mul, evalβ_mul_noncomm, natDegree_list_prod_le, derivative_C_mul_X_sq, card_support_trinomial, trailingCoeff_mul, Splits.listProd, IsMonicOfDegree.of_dvd_sub, exists_mul_add_mul_eq_C_resultant, Matrix.charpoly_of_card_eq_two, smeval_mul_X_pow, trailingDegree_mul, X_pow_mul_C, RatFunc.num_denom_neg, degree_mul, isMonicOfDegree_sub_add_two, X_pow_mul, Monic.neg_one_pow_natDegree_mul_comp_neg_X, Monic.natDegree_mul'
|
instNSMul π | CompOp | 21 mathmath: one_add_X_pow_sub_X_pow, iterate_derivative_eq_factorial_smul_sum, iterate_derivative_X_add_pow, iterate_derivative_mul_X, Real.Polynomial.isRoot_cos_pi_div_five, iterate_derivative_X_sub_pow, ascPochhammer_succ_comp_X_add_one, natCast_mul, iterate_derivative_derivative_mul_X_sq, toFinsupp_nsmul, exists_iterate_derivative_eq_factorial_smul, bernsteinPolynomial.variance, iterate_derivative_derivative_mul_X, bernsteinPolynomial.sum_smul, bernoulli_eq_sub_sum, bernoulli_comp_one_add_X, bernsteinPolynomial.sum_mul_smul, iterate_derivative_mul_X_pow, iterate_derivative_mul, bernoulli_comp_neg_X, ofFinsupp_nsmul
|
instNatCast π | CompOp | 84 mathmath: Chebyshev.one_sub_X_sq_mul_derivative_derivative_U_eq_poly_in_U, WeierstrassCurve.Οβ_sq, descPochhammer_succ_comp_X_sub_one, derivative_expand, chebyshev_U_eq_dickson_two_one, Matrix.charpoly_natCast, Chebyshev.S_eq_X_mul_S_add_C, Chebyshev.S_comp_two_mul_X, ofFinsupp_natCast, Chebyshev.T_two, Chebyshev.T_add_one, natCast_mul, Chebyshev.C_eq_S_sub_X_mul_S, C_eq_natCast, Chebyshev.U_two, Chebyshev.U_eq, evalβ_natCast, eval_natCast, ascPochhammer_mul, descPochhammer_succ_right, Chebyshev.U_sub_one, iterate_derivative_natCast_mul, Chebyshev.U_one, smeval_natCast, Mathlib.Tactic.ComputeDegree.natDegree_natCast_le, natTrailingDegree_natCast, derivative_natCast_mul, natCast_coeff_zero, coeff_natCast_ite, WeierstrassCurve.C_Ξ¨βSq, iterate_derivative_X_pow_eq_natCast_mul, coeff_natCast_mul, Chebyshev.T_eq, descPochhammer_eq_ascPochhammer, bernsteinPolynomial.variance, descPochhammer_mul, toFinsupp_natCast, Matrix.charmatrix_natCast, Lagrange.iterate_derivative_interpolate, Chebyshev.U_add_two, natCast_inj, iterate_derivative_prod_X_sub_C, factorial_mul_shiftedLegendre_eq, Chebyshev.T_neg_two, eval_natCast_mul, dickson_one_one_eq_chebyshev_T, chebyshev_T_eq_dickson_one_one, mul_X_add_natCast_comp, natDegree_natCast, Chebyshev.C_comp_two_mul_X, Chebyshev.one_sub_X_sq_mul_iterate_derivative_T_eq_poly_in_T, Chebyshev.U_add_one, ofNat_comp, natCast_comp, geom_sum_X_comp_X_add_one_eq_sum, Chebyshev.T_mul_T, Chebyshev.T_sub_one, bernsteinPolynomial.derivative_succ, coeff_mul_natCast, iterate_derivative_X_sub_pow_self, Chebyshev.C_zero, dickson_zero, derivative_bernoulli_add_one, Chebyshev.U_sub_two, Chebyshev.C_eq_two_mul_T_comp_half_mul_X, Chebyshev.T_eq_half_mul_C_comp_two_mul_X, dickson_two, mul_X_sub_intCast_comp, Chebyshev.T_sub_two, derivative_natCast, derivative_bernoulli, Chebyshev.T_add_two, natCast_mul_comp, bernsteinPolynomial.derivative_zero, map_natCast, aeval_natCast, Chebyshev.one_sub_X_sq_mul_iterate_derivative_U_eq_poly_in_U, evalEval_natCast, Chebyshev.C_two, bernsteinPolynomial.derivative_succ_aux, Chebyshev.C_neg_two, WeierstrassCurve.Ξ¨_odd, ascPochhammer_succ_right, degree_natCast_le
|
instNeg π | CompOp | 78 mathmath: Multiset.prod_X_sub_X_eq_sum_esymm, derivative_comp_one_sub_X, splits_neg_iff, mirror_neg, comp_neg_X_eq_zero_iff, Chebyshev.S_neg_sub_two, Matrix.charmatrix_apply_ne, natDegree_neg_le_of_le, support_neg, wronskian_neg_right, WeierstrassCurve.Ξ¨_neg, WeierstrassCurve.Affine.addPolynomial_slope, WeierstrassCurve.Affine.C_addPolynomial_slope, iterate_derivative_comp_one_sub_X, wronskian_neg_eq, Matrix.charmatrix_fromBlocks, degree_neg_le_of_le, Chebyshev.U_neg_sub_one, WeierstrassCurve.Affine.derivative_addPolynomial_slope, WeierstrassCurve.Affine.addPolynomial_eq, neg_modByMonic, comp_neg_X_leadingCoeff_eq, algEquivAevalNegX_symm_apply, mul_comp_neg_X, neg_cancelLeads, Chebyshev.S_neg_two, Chebyshev.U_neg, Chebyshev.S_neg, ofFinsupp_neg, reflect_neg, WeierstrassCurve.Ο_neg, monomial_neg, natTrailingDegree_neg, aeval_neg, degree_neg, coe_neg, evalEval_neg, WeierstrassCurve.preΞ¨_neg, iterate_derivative_neg, degree_comp_neg_X, minpoly.neg, reverse_neg, WeierstrassCurve.Affine.CoordinateRing.coe_norm_smul_basis, toFinsupp_neg, aroots_neg, evalβ_neg, coeffList_neg, coeff_neg, derivative_neg, dvd_comp_neg_X_iff, Matrix.charpoly_inv, algEquivAevalNegX_apply, roots_neg, signVariations_neg, eval_neg, map_neg, Chebyshev.U_neg_two, Chebyshev.S_neg_sub_one, natDegree_neg, C_neg, neg_comp, bernsteinPolynomial.derivative_zero, Splits.comp_neg_X, bernoulli_comp_one_sub_X, Splits.neg, smeval_neg, wronskian_neg_left, trailingDegree_neg, bernoulli_comp_neg_X, comp_neg_X_comp_neg_X, WeierstrassCurve.Ξ¨_odd, leadingCoeff_neg, neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq, homogenize_neg, Chebyshev.U_neg_sub_two, RatFunc.num_denom_neg, rootSet_neg, Monic.neg_one_pow_natDegree_mul_comp_neg_X
|
instOne π | CompOp | 242 mathmath: logMahlerMeasure_one, Lagrange.interpolate_one, coe_eq_one_iff, primPart_zero, LaurentPolynomial.mk'_one_X_pow, map_one, one_add_X_pow_sub_X_pow, eq_cyclotomic_iff, StandardEtalePair.inv_aeval_X_g, splits_X_pow_sub_one_of_X_pow_sub_C, resultant_one_right, coeff_one, cyclotomic_six, Chebyshev.one_sub_X_sq_mul_derivative_derivative_U_eq_poly_in_U, Multiset.prod_X_sub_X_eq_sum_esymm, RatFunc.num_one, leadingCoeff_one, C_1, derivative_comp_one_sub_X, contentIdeal_one, descPochhammer_succ_comp_X_sub_one, leadingCoeff_det_X_one_add_C, RatFunc.denom_one, coeff_one_add_X_pow, irreducible_of_monic, StandardEtalePresentation.toPresentation_algebra_smul, LaurentPolynomial.mk'_one_X, eq_one_of_roots_le, WeierstrassCurve.Ξ¨Sq_odd, derivative_X, evalβ_one, coe_one, restriction_one, degree_list_prod, modByMonic_one, map_list_prod, Lagrange.basis_singleton, Matrix.derivative_det_one_add_X_smul, integralNormalization_C, prod_cyclotomic_eq_X_pow_sub_one, degree_list_prod_le, Monic.natDegree_eq_zero, WeierstrassCurve.Affine.polynomial_eq, WeierstrassCurve.preΞ¨'_one, WeierstrassCurve.preΞ¨_odd, one_scaleRoots, WeierstrassCurve.Ξ¨_one, Lagrange.nodal_empty, Matrix.det_one_add_smul, Lagrange.basisDivisor_add_symm, Chebyshev.T_two, ascPochhammer_succ_comp_X_add_one, WeierstrassCurve.Ξ¨Sq_ofNat, evalβ_list_prod, aeval_one, cyclotomic_two, Chebyshev.U_two, Chebyshev.S_sq_add_S_sq, X_pow_sub_one_dvd_prod_cyclotomic, aeval_homogenize_X_one, StandardEtalePair.equivMvPolynomialQuotient_symm_apply, cyclotomic'_one, X_pow_sub_one_eq_prod, mkDerivation_one_eq_derivative', derivative_X_add_C, Real.fibRec_charPoly_eq, RatFunc.ofFractionRing_one, hermite_eq_iterate, WeierstrassCurve.Ξ¨_ofNat, splits_one, gal_X_pow_sub_one_isSolvable, bernsteinPolynomial.flip', ofFinsupp_eq_one, list_prod_comp, Chebyshev.one_sub_X_sq_mul_derivative_T_eq_poly_in_T, reflect_one, bernoulli_zero, X_pow_sub_X_sub_one_irreducible, iterate_derivative_comp_one_sub_X, prod_cyclotomic'_eq_X_pow_sub_one, IsCyclotomicExtension.isSplittingField_X_pow_sub_one, Lagrange.basis_empty, IsPrimitiveRoot.minpoly_sub_one_eq_cyclotomic_comp, Monic.isUnit_iff, ofFinsupp_one, Monic.natDegree_eq_zero_iff_eq_one, IsCyclotomicExtension.splits_X_pow_sub_one, Chebyshev.U_zero, natTrailingDegree_one, bernsteinPolynomial.flip, eval_list_prod, FixedPoints.minpoly.irreducible_aux, reflect_one_X, separable_def', Matrix.charpoly_one, Matrix.det_one_add_X_smul, descPochhammer_eq_ascPochhammer, toFinsupp_one, cyclotomic_prime_pow_mul_X_pow_sub_one, separable_one, bernsteinPolynomial.variance, cauchyBound_one, Chebyshev.add_one_mul_self_mul_T_eq_poly_in_T, descPochhammer_succ_left, AdjoinRoot.root_isInv, monomial_zero_one, RatFunc.one_def, isMonicOfDegree_zero_iff, cyclotomic_zero, cyclotomic.dvd_X_pow_sub_one, Chebyshev.S_neg_two, Chebyshev.S_zero, bernoulli_comp_one_add_X, WeierstrassCurve.Ξ¦_ofNat, degree_one_le, minpoly.subsingleton, X_pow_sub_one_separable_iff, WeierstrassCurve.Ο_one, RatFunc.denom_X, content_one, WeierstrassCurve.preΞ¨'_odd, hilbertPoly_mul_one_sub_succ, cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt, smeval_one, natDegree_one, degree_one, ascPochhammer_zero, X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd, factorial_mul_shiftedLegendre_eq, Chebyshev.one_sub_X_sq_mul_derivative_derivative_T_eq_poly_in_T, comp_one, coeffs_one, natSepDegree_one, dvd_C_mul_X_sub_one_pow_add_one, WeierstrassCurve.Ξ¨Sq_one, Chebyshev.T_neg_two, isPrimitive_one, Chebyshev.S_two, gal_one_isSolvable, toFinsupp_eq_one, Matrix.charpoly_isEmpty, cyclotomic_one, mahlerMeasure_one, PolyEquivTensor.invFun_monomial, one_comp, mkDerivation_one_eq_derivative, PolyEquivTensor.toFunLinear_one_tmul_one, StandardEtalePresentation.toPresentation_Ο', roots_list_prod, cyclotomic_eq_prod_X_pow_sub_one_pow_moebius, coeff_X_add_one_pow, RatFunc.denom_C, LinearMap.charpoly_one, FiniteField.minpoly_frobeniusAlgHom, Matrix.charmatrix_one, Matrix.coeff_det_one_add_X_smul_one, Chebyshev.one_sub_X_sq_mul_iterate_derivative_T_eq_poly_in_T, X_pow_sub_X_sub_one_irreducible_rat, trailingDegree_one, cyclotomic'_two, AdjoinRoot.algHom_subsingleton, toLaurent_one, Chebyshev.one_sub_X_sq_mul_U_eq_pol_in_T, minpoly.one, geom_sum_X_comp_X_add_one_eq_sum, minpoly.neg, RatFunc.algebraMap_apply, PowerSeries.trunc_one, roots_one, rootSet_one, StandardEtalePair.aeval_X_g_mul_mk_X, hasseDeriv_apply_one, RatFunc.mk_one, eval_one, derivativeFinsupp_one, Matrix.charpoly_inv, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, RatFunc.denom_algebraMap, Mathlib.Tactic.ComputeDegree.natDegree_one_le, derivative_bernoulli_add_one, Lagrange.sum_basis, StandardEtalePresentation.toPresentation_val, Chebyshev.T_zero, leadingCoeff_X_pow_sub_one, aroots_one, not_isUnit_X_pow_sub_one, cyclotomic_three, RatFunc.mk_one', Chebyshev.U_neg_two, IsLocalization.adjoin_inv, monic_one, cyclotomic_comp_X_add_one_isEisensteinAt, leadingCoeff_X_pow_add_one, evalEval_list_prod, Chebyshev.T_eq_X_mul_T_sub_pol_U, resultant_one_left, bernsteinPolynomial.sum, Lagrange.nodal_subgroup_eq_X_pow_card_sub_one, StandardEtalePresentation.toPresentation_relation, WeierstrassCurve.preΞ¨_two, Monic.eq_one_of_isUnit, eq_one_of_monic_natDegree_zero, hilbertPoly_mul_one_sub_pow_add, divX_one, X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd, iterate_derivative_one, Chebyshev.one_sub_X_sq_mul_iterate_derivative_U_eq_poly_in_U, bernoulli_comp_one_sub_X, matPolyEquiv_smul_one, WeierstrassCurve.preΞ¨_one, cyclotomic_eq_X_pow_sub_one_div, Matrix.derivative_det_one_add_X_smul_aux, bernsteinPolynomial.derivative_succ_aux, WeierstrassCurve.Ο_zero, derivative_X_sub_C, coeff_one_zero, cyclotomic_prime_mul_X_sub_one, ascPochhammer_succ_left, WeierstrassCurve.Ξ¦_zero, trailingDegree_one_le, homogenize_one, derivative_one, evalβ_list_prod_noncomm, Monic.degree_le_zero_iff_eq_one, descPochhammer_zero, divByMonic_one, evalEval_one, neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq, RatFunc.denom_zero, WeierstrassCurve.preΞ¨'_two, coeff_list_prod_of_natDegree_le, Chebyshev.add_one_mul_T_eq_poly_in_U, natDegree_list_prod_le, taylor_one, cyclotomic'_zero, derivativeFinsupp_X, Splits.listProd, Splits.one, IsPrimitiveRoot.minpoly_dvd_x_pow_sub_one, cyclotomic'_eq_X_pow_sub_one_div, Monic.neg_one_pow_natDegree_mul_comp_neg_X, toSubring_one
|
instSub π | CompOp | 443 mathmath: mul_div_eq_iff_isRoot, IsAdjoinRoot.repr_add_sub_repr_add_repr_mem_span, eq_X_sub_C_of_separable_of_root_eq, separable_X_pow_sub_C_unit, splits_iff_exists_multiset, Chebyshev.T_eq_X_mul_U_sub_U, reflect_sub, taylorWithin_succ, mul_divByMonic_eq_iff_isRoot, monic_X_sub_C, one_add_X_pow_sub_X_pow, eq_cyclotomic_iff, ker_evalRingHom, StandardEtalePair.inv_aeval_X_g, IsPurelyInseparable.minpoly_eq', root_X_sub_C, X_pow_sub_C_splits_of_isPrimitiveRoot, pow_rootMultiplicity_dvd, X_pow_sub_C_eq_prod, expNegInvGlue.hasDerivAt_polynomial_eval_inv_mul, cyclotomic_six, Chebyshev.one_sub_X_sq_mul_derivative_derivative_U_eq_poly_in_U, WeierstrassCurve.Ξ¨Sq_even, prod_X_sub_C_nextCoeff, mem_roots_sub_C', Multiset.prod_X_sub_X_eq_sum_esymm, exists_partition_polynomial, aroots_X_sub_C, natDegree_sub_le_iff_right, prod_multiset_X_sub_C_of_monic_of_roots_card_eq, IsMonicOfDegree.natDegree_sub_X_pow, derivative_comp_one_sub_X, monic_multisetProd_X_sub_C, isCoprime_of_is_root_of_eval_derivative_ne_zero, descPochhammer_succ_comp_X_sub_one, quotientSpanXSubCAlgEquiv_symm_apply, X_pow_sub_C_irreducible_iff_of_odd, zero_notMem_multiset_map_X_sub_C, card_roots_sub_C', Irreducible.natSepDegree_eq_one_iff_of_monic', X_pow_sub_C_irreducible_of_odd, StandardEtalePresentation.toPresentation_algebra_smul, coeff_sub_eq_left_of_lt, natDegree_X_pow_sub_C, Monic.natSepDegree_eq_one_iff_of_irreducible', WeierstrassCurve.Ξ¨Sq_odd, eq_prod_roots_of_splits, eq_prod_roots_of_monic_of_splits_id, WeierstrassCurve.Affine.Y_sub_negPolynomial, minpoly_algHom_toLinearMap, Lagrange.interpolate_eq_nodalWeight_mul_nodal_div_X_sub_C, natSepDegree_X_sub_C_pow, isMonicOfDegree_two_iff', exists_partition_polynomial_aux, IsMonicOfDegree.natDegree_sub_lt, Monic.eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one, minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C, natDegree_sub_eq_right_of_natDegree_lt, isMonicOfDegree_X_sub_one, ConjRootClass.minpoly.map_eq_prod, Chebyshev.S_add_one, coeff_divByMonic_X_sub_C_rec, Subfield.splits_bot, Matrix.charmatrix_apply_eq, Lagrange.nodal_insert_eq_nodal, Matrix.charpoly_natCast, eval_divByMonic_eq_trailingCoeff_comp, X_pow_sub_C_irreducible_iff_forall_prime_of_odd, rootMultiplicity_X_sub_C_pow, resultant_X_sub_C_right, monic_finprod_X_sub_C, Real.Polynomial.isRoot_cos_pi_div_five, WeierstrassCurve.Affine.C_addPolynomial, self_sub_monomial_natDegree_leadingCoeff, natDegree_finset_prod_X_sub_C_eq_card, prod_cyclotomic_eq_X_pow_sub_one, pow_rootMultiplicity_not_dvd, divByMonic_add_X_sub_C_mul_derivative_divByMonic_eq_derivative, Chebyshev.S_eq, WeierstrassCurve.preΞ¨_odd, dvd_comp_X_add_C_iff, separable_X_pow_sub_C, dvd_comp_C_mul_X_add_C_iff, X_pow_sub_one_splits, Monic.comp_X_sub_C, degree_X_sub_C, iterate_derivative_X_sub_pow, isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top, PowerSeries.IsWeierstrassFactorization.isWeierstrassDivision, exists_finset_of_splits, Chebyshev.T_two, ofFinsupp_sub, Matrix.charpoly_of_upperTriangular, Chebyshev.T_add_one, gal_X_pow_sub_C_isSolvable, Lagrange.interpolate_eq_sum, FiniteField.roots_X_pow_card_sub_X, Chebyshev.C_eq_S_sub_X_mul_S, WeierstrassCurve.Ο_three, AdjoinRoot.mk_eq_mk, derivative_X_sub_C_sq, FiniteField.instIsSplittingFieldExtensionHSubPolynomialHPowNatXCard, Chebyshev.U_two, roots_X_pow_char_pow_sub_C_pow, Multiset.prod_X_sub_C_dvd_iff_le_roots, Matrix.IsHermitian.charpoly_cfc_eq, mem_span_C_X_sub_C_X_sub_C_iff_eval_eval_eq_zero, Chebyshev.U_eq, Chebyshev.S_sq_add_S_sq, X_pow_sub_one_dvd_prod_cyclotomic, prod_multiset_root_eq_finset_root, X_pow_sub_C_separable_iff, IsPurelyInseparable.minpoly_eq, coeff_X_sub_C_mul, monic_X_pow_sub_C, rootMultiplicity_eq_natFind_of_ne_zero, StandardEtalePair.equivMvPolynomialQuotient_symm_apply, cyclotomic'_one, WeierstrassCurve.preΞ¨'_even, logMahlerMeasure_X_sub_C, X_pow_sub_one_eq_prod, prod_multiset_X_sub_C_dvd, AdjoinRoot.mul_div_root_cancel, minpoly.natSepDegree_eq_one_iff_eq_X_sub_C_pow, hermite_succ, descPochhammer_succ_right, Chebyshev.U_sub_one, Real.fibRec_charPoly_eq, hermite_eq_iterate, WeierstrassCurve.Affine.CoordinateRing.C_addPolynomial, cyclotomic_eq_prod_X_sub_primitiveRoots, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_add_eq, Splits.comp_X_sub_C, coeff_mul_X_sub_C, smeval_sub, gal_X_pow_sub_one_isSolvable, natSepDegree_C_mul_X_sub_C_pow, X_sub_C_mul_divByMonic_eq_sub_modByMonic, roots_C_mul_X_sub_C_of_IsUnit, bernsteinPolynomial.flip', WeierstrassCurve.Affine.addPolynomial_slope, rootMultiplicity_eq_nat_find_of_nonzero, derivative_X_sub_C_pow, X_pow_sub_C_irreducible_iff_of_prime_pow, Lagrange.basis_eq_prod_sub_inv_mul_nodal_div, natDegree_sub_le_of_le, IsRoot.mul_div_eq, Chebyshev.one_sub_X_sq_mul_derivative_T_eq_poly_in_T, MulSemiringAction.charpoly_eq_prod_smul, X_pow_sub_X_sub_one_irreducible, leadingCoeff_X_pow_sub_C, coeff_sub_eq_neg_right_of_lt, minpoly.eq_X_sub_C_of_algebraMap_inj, WeierstrassCurve.Affine.C_addPolynomial_slope, iterate_derivative_comp_one_sub_X, Splits.eq_prod_roots, div_wf_lemma, exists_approx_polynomial_aux, prod_cyclotomic'_eq_X_pow_sub_one, WeierstrassCurve.Affine.CoordinateRing.norm_smul_basis, IsCyclotomicExtension.isSplittingField_X_pow_sub_one, evalβ_sub, natDegree_sub_le_iff_left, separable_X_pow_sub_C', IsCyclotomicExtension.splits_X_pow_sub_one, Chebyshev.S_sub_one, Splits.eq_X_sub_C_of_single_root, bernsteinPolynomial.flip, modByMonic_eq_sub_mul_div, quotientSpanXSubCAlgEquiv_mk, Lagrange.X_sub_C_dvd_nodal, roots_X_sub_C, WeierstrassCurve.C_Ξ¨βSq, le_rootMultiplicity_iff, WeierstrassCurve.Affine.derivative_addPolynomial_slope, rootMultiplicity_mul_X_sub_C_pow, Matrix.charpoly_one, Subfield.roots_X_pow_char_sub_X_bot, natSepDegree_X_pow_char_pow_sub_C, evalEval_sub, FiniteField.isSplittingField_of_nat_card_eq, degree_X_pow_sub_C, Chebyshev.T_eq, descPochhammer_eq_ascPochhammer, Irreducible.natSepDegree_eq_one_iff_of_monic, Chebyshev.C_eq, WeierstrassCurve.Ο_even, cyclotomic_prime_pow_mul_X_pow_sub_one, resultant_X_sub_C_pow_left, bernsteinPolynomial.variance, eval_iterate_derivative_rootMultiplicity, Chebyshev.add_one_mul_self_mul_T_eq_poly_in_T, sub_mod, bernoulli_eq_sub_sum, descPochhammer_succ_left, separable_prod_X_sub_C_iff', descPochhammer_mul, AdjoinRoot.root_isInv, FiniteField.splits_X_pow_nat_card_sub_X, eq_prod_roots_of_splits_id, natDegree_X_sub_C, Matrix.matPolyEquiv_charmatrix, resultant_X_sub_C_pow_right, X_sub_C_dvd_sub_C_eval, WeierstrassCurve.Affine.Y_sub_polynomialY, prime_X_sub_C, Matrix.charmatrix_natCast, Lagrange.iterate_derivative_interpolate, C_sub, roots_X_pow_char_sub_C_pow, quadratic_dvd_of_aeval_eq_zero_im_ne_zero, algEquivAevalXAddC_symm_apply, nextCoeff_X_sub_C, degree_X_sub_C_le, cyclotomic.dvd_X_pow_sub_one, Monic.natSepDegree_eq_one_iff, X_pow_sub_C_irreducible_of_prime, roots_multiset_prod_X_sub_C, Matrix.charpoly_fin_two, separable_prod_X_sub_C_iff, dickson_add_two, exists_eq_pow_rootMultiplicity_mul_and_not_dvd, leadingCoeff_sub_of_degree_lt, WeierstrassCurve.Ξ¦_ofNat, exists_approx_polynomial, Chebyshev.C_sub_one, card_roots_X_pow_sub_C, X_pow_sub_one_separable_iff, mem_roots_sub_C, WeierstrassCurve.Ξ¦_three, Chebyshev.U_add_two, isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow, WeierstrassCurve.preΞ¨'_odd, gal_X_sub_C_isSolvable, hilbertPoly_mul_one_sub_succ, FiniteField.isSplittingField_of_card_eq, natDegree_multiset_prod_X_sub_C_eq_card, Matrix.charpoly_coeff_eq_prod_coeff_of_le, iterate_derivative_prod_X_sub_C, signVariations_eraseLead_mul_X_sub_C, X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd, natDegree_sub_eq_left_of_natDegree_lt, mahlerMeasure_X_sub_C, minpoly.add_algebraMap, MulSemiringAction.charpoly_eq, WeierstrassCurve.Ο_odd, root_X_pow_sub_C_pow, WeierstrassCurve.Ξ¨_even, natDegree_sub, WeierstrassCurve.Ξ¦_four, Chebyshev.C_add_one, factorial_mul_shiftedLegendre_eq, Chebyshev.one_sub_X_sq_mul_derivative_derivative_T_eq_poly_in_T, dvd_C_mul_X_sub_one_pow_add_one, Monic.sub_of_left, isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C, ofMultiset_apply, Cubic.prod_X_sub_C_eq, Chebyshev.T_neg_two, rootMultiplicity_eq_multiplicity, multiset_prod_X_sub_C_nextCoeff, Chebyshev.S_two, Lagrange.nodal_eq_mul_nodal_erase, AlgebraicClosure.Monics.map_eq_prod, cyclotomic_one, Monic.sub_of_right, FiniteField.X_pow_card_sub_X_natDegree_eq, not_isUnit_X_sub_C, FiniteField.splits_X_pow_card_sub_X, coeff_sub, degree_sub_le, Matrix.charpoly_sub_diagonal_degree_lt, Splits.X_sub_C, sub_modByMonic, C_leadingCoeff_mul_prod_multiset_X_sub_C, minpoly.eq_X_sub_C', leadingCoeff_sub_of_degree_eq, StandardEtalePresentation.toPresentation_Ο', cyclotomic_eq_prod_X_pow_sub_one_pow_moebius, iterate_derivative_sub, eq_X_sub_C_of_splits_of_single_root, Mathlib.Tactic.ComputeDegree.coeff_sub_of_eq, modByMonic_X_sub_C_eq_C_eval, Matrix.charpoly_vecMulVec, coe_sub, Splits.eq_prod_roots_of_monic, leadingCoeff_X_sub_C, WeierstrassCurve.Ξ¦_two, IsPurelyInseparable.minpoly_eq_X_pow_sub_C, LinearMap.charpoly_one, natDegree_X_sub_C_le, splits_X_sub_C_mul_iff, FiniteField.minpoly_frobeniusAlgHom, dickson_of_two_le, Matrix.charmatrix_one, Chebyshev.one_sub_X_sq_mul_iterate_derivative_T_eq_poly_in_T, Chebyshev.U_add_one, X_sub_C_scaleRoots, X_pow_sub_X_sub_one_irreducible_rat, sum_taylor_eq, degree_sub_eq_left_of_degree_lt, minpoly_algEquiv_toLinearMap, AdjoinRoot.algHom_subsingleton, mod_X_sub_C_eq_C_eval, Chebyshev.one_sub_X_sq_mul_U_eq_pol_in_T, minpoly.one, derivative_sub, natSepDegree_X_sub_C, WeierstrassCurve.Affine.CoordinateRing.coe_norm_smul_basis, Chebyshev.T_sub_one, spectralValue_X_sub_C, StandardEtalePair.aeval_X_g_mul_mk_X, map_sub, roots_C_mul_X_sub_C, rootMultiplicity_le_iff, eraseLead_mul_eq_mul_eraseLead_of_nextCoeff_zero, IsPurelyInseparable.minpoly_eq_X_sub_C_pow, X_pow_sub_C_irreducible_of_prime_pow, bernsteinPolynomial.derivative_succ, PowerSeries.IsWeierstrassDivision.isWeierstrassFactorization, iterate_derivative_X_sub_pow_self, X_dvd_sub_C, eval_mul_X_sub_C, minpolyDiv_spec, Monic.eq_X_pow_char_pow_sub_C_of_natSepDegree_eq_one_of_irreducible, natDegree_sub_C, toFinsupp_sub, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, dickson_zero, signVariations_X_sub_C_mul_eraseLead_le, roots_X_pow_char_sub_C, bernoulli_one, degree_sub_lt, StandardEtalePresentation.toPresentation_val, Chebyshev.U_sub_two, leadingCoeff_X_pow_sub_one, homogenize_sub, FiniteField.X_pow_card_pow_sub_X_natDegree_eq, WeierstrassCurve.Ο_four, rootMultiplicity_X_sub_C_self, splits_X_sub_C, algEquivCMulXAddC_symm_apply, IsMonicOfDegree.aeval_sub, not_isUnit_X_pow_sub_one, dickson_two, succ_signVariations_X_sub_C_mul_monomial, rootMultiplicity_X_sub_C, IsLocalization.adjoin_inv, dvd_comp_X_sub_C_iff, pow_mul_divByMonic_rootMultiplicity_eq, Chebyshev.C_sub_two, X_sub_C_mul_removeFactor, Cubic.eq_prod_three_roots, FiniteField.isSplittingField_sub, leadingCoeff_sub_of_degree_lt', exists_prod_multiset_X_sub_C_mul, Matrix.charmatrix_apply, mul_X_sub_intCast_comp, Chebyshev.T_sub_two, Matrix.charmatrix_ofNat, minpoly.natSepDegree_eq_one_iff_eq_expand_X_sub_C, dvd_iff_isRoot, Chebyshev.T_eq_X_mul_T_sub_pol_U, cauchyBound_X_sub_C, splits_of_exists_multiset, prod_X_sub_C_coeff_card_pred, Chebyshev.S_add_two, Chebyshev.C_add_two, WeierstrassCurve.Ο_two, resultant_X_sub_C_left, Lagrange.nodal_subgroup_eq_X_pow_card_sub_one, Chebyshev.T_add_two, StandardEtalePresentation.toPresentation_relation, hilbertPoly_mul_one_sub_pow_add, mul_star_dvd_of_aeval_eq_zero_im_ne_zero, X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd, Matrix.IsHermitian.charpoly_eq, multiset_prod_X_sub_C_coeff_card_pred, separable_X_sub_C, finiteMultiplicity_X_sub_C, irreducible_X_sub_C, preimage_eval_singleton, IsMonicOfDegree.sub, Cubic.C_mul_prod_X_sub_C_eq, Chebyshev.one_sub_X_sq_mul_iterate_derivative_U_eq_poly_in_U, bernoulli_comp_one_sub_X, eval_sub, Chebyshev.C_two, succ_signVariations_le_X_sub_C_mul, monomial_sub, PowerSeries.trunc_sub, IsMonicOfDegree.of_dvd_add, degree_sub_le_of_le, autAdjoinRootXPowSubC_root, Matrix.charpoly_diagonal, natDegree_sub_le, Monic.natSepDegree_eq_one_iff_of_irreducible, matPolyEquiv_eq_X_pow_sub_C, cyclotomic_eq_X_pow_sub_one_div, coeff_divByMonic_X_sub_C, Matrix.charpoly_ofNat, leadingCoeff_divByMonic_X_sub_C, bernsteinPolynomial.derivative_succ_aux, pairwise_coprime_X_sub_C, derivative_X_sub_C, Chebyshev.T_eq_U_sub_X_mul_U, minpoly.eq_X_sub_C, cyclotomic_prime_mul_X_sub_one, Chebyshev.C_neg_two, Matrix.charmatrix_diagonal, Lagrange.nodal_erase_eq_nodal_div, monic_prod_X_sub_C, WeierstrassCurve.Ξ¨_odd, aeval_sub, card_roots_sub_C, self_sub_C_mul_X_pow, isCoprime_X_sub_C_of_isUnit_sub, irreducible_X_pow_sub_C_of_root_adjoin_eq_top, neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq, Chebyshev.S_sub_two, galois_poly_separable, WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_Y, WeierstrassCurve.preΞ¨_even, Chebyshev.add_one_mul_T_eq_poly_in_U, Lagrange.nodal_eq, X_pow_sub_C_irreducible_iff_of_prime, roots_X_pow_char_pow_sub_C, sub_comp, Matrix.charpoly_of_card_eq_two, eval_multiset_prod_X_sub_C_derivative, X_sub_C_pow_dvd_iff, isCyclic_tfae, roots_prod_X_sub_C, degree_sub_C, Multiset.prod_X_sub_C_coeff, IsPrimitiveRoot.minpoly_dvd_x_pow_sub_one, isMonicOfDegree_sub_add_two, cyclotomic'_eq_X_pow_sub_one_div, degree_sub_eq_right_of_degree_lt, GaloisField.splits_zmod_X_pow_sub_X, monic_X_pow_sub, Monic.eq_X_sub_C_pow_of_natSepDegree_eq_one_of_splits, Matrix.isNilpotent_charpoly_sub_pow_of_isNilpotent
|
instZSMul π | CompOp | 3 mathmath: toFinsupp_zsmul, ofFinsupp_zsmul, bernoulli_comp_neg_X
|
instZero π | CompOp | 342 mathmath: isUnit_C_add_X_mul_iff, isLeftCancelMulZero_iff, eraseLead_monomial, primPart_zero, ofFn_zero, toLaurent_eq_zero, cardPowDegree_zero, ofFinsupp_zero, coeff_natTrailingDegree_eq_zero, divX_X_pow, degree_smul_of_smul_regular, iterate_derivative_zero, Mathlib.Tactic.ComputeDegree.degree_smul_le_of_le, wronskian_self_eq_zero, eraseLead_natDegree_lt_or_eraseLead_eq_zero, PowerSeries.trunc_X_pow_self_mul, eraseLead_X_pow, divByMonic_eq_of_not_monic, nnqsmul_eq_C_mul, PowerSeries.zero_weierstrassMod, homogenize_smul, sum_smul_index', derivative_pow_eq_zero, leadingCoeff_det_X_one_add_C, zero_notMem_multiset_map_X_sub_C, derivative_ofNat, derivative_smul, nextCoeffUp_zero, isNilpotent_X_mul_iff, natDegree_smul, comp_neg_X_eq_zero_iff, Mathlib.Tactic.ComputeDegree.natDegree_zero_le, resultant_zero_right, content_eq_zero_iff, C_mul', content_zero, hilbertPoly_eq_zero_of_le_rootMultiplicity_one, matPolyEquiv_diagonal_X, length_coeffList_eq_ite, evalβ_zero, supNorm_zero, zero_comp, modByMonic_one, instIsRightCancelMulZeroOfIsCancelAdd, divByMonic_eq_zero_iff, reverse_eq_zero, WeierstrassCurve.preΞ¨'_zero, coe_eq_zero_iff, Matrix.derivative_det_one_add_X_smul, roots_zero, rootMultiplicity_eq_zero_iff, monic_of_isUnit_leadingCoeff_inv_smul, iterate_derivative_X, AdjoinRoot.smul_mk, Lagrange.basisDivisor_self, WeierstrassCurve.Affine.polynomial_eq, natDegree_smul_of_smul_regular, leadingCoeff_zero, C_eq_zero, isRightCancelMulZero_iff, Gal.restrictDvd_def, evalβ_list_sum, Matrix.det_one_add_smul, coeff_list_sum_map, smul_monomial, gaussNorm_eq_zero_iff, splits_zero, C_0, sum_smul_index, isCancelMulZero_iff, matPolyEquiv_coeff_apply_aux_1, smul_eq_C_mul, isScalarTower, derivativeFinsupp_apply_toFun, zero_divByMonic, cauchyBound_smul, comp_C_mul_X_eq_zero_iff, modByMonic_eq_zero_iff_quotient_eq_zero, natSepDegree_zero, coeffs_empty_iff, IsFractionRing.integerNormalization_eq_zero_iff, gaussNorm_zero, signVariations_zero, not_monic_zero, denomsClearable_zero, isUnit_iff', Matrix.charmatrix_blockTriangular_iff, monomial_eq_zero_iff, mahlerMeasure_eq_zero_iff, smeval_smul, trailingDegree_zero, prodXSubSMul.smul, eq_zero_of_natDegree_lt_card_of_eval_eq_zero', Cubic.of_d_eq_zero, restriction_zero, toFinsupp_eq_zero, not_separable_zero, modByMonic_eq_zero_iff_dvd, RatFunc.ofFractionRing_zero, eraseLead_C_mul_X, IsSMulRegular.polynomial, natTrailingDegree_eq_zero, divX_eq_zero_iff, MulSemiringAction.charpoly_eq_prod_smul, taylor_eq_zero, natDegree_list_sum_le, eq_zero_of_eq_zero, natDegree_eq_support_max', derivativeFinsupp_apply_apply, noZeroDivisors_iff, notMem_nonZeroDivisors_iff, Splits.zero, MulSemiringAction.smul_charpoly, derivativeFinsupp_derivative, RatFunc.num_zero, hilbertPoly_zero_left, Matrix.GeneralLinearGroup.fixpointPolynomial_eq_zero_iff, Chebyshev.U_eq_zero_iff, PowerSeries.IsWeierstrassDivision.eq_zero, Mathlib.Tactic.ComputeDegree.natDegree_smul_le_of_le, zero_of_eval_zero, eq_zero_of_forall_eval_zero_of_natDegree_lt_card, rootSet_zero, Splits.def, smul_X, coe_smul, splits_iff, Lagrange.basisDivisor_eq_zero_iff, smul_eq_map, derivative_of_natDegree_zero, Matrix.det_one_add_X_smul, smul_eval_smul, comp_eq_zero_iff, iterate_derivative_C, toFn_zero, ofFn_zero', natDegree_zero, iterate_derivative_eq_zero, Monic.mul_right_eq_zero_iff, isCentralScalar, WeierstrassCurve.preΞ¨_zero, self_mul_modByMonic, degree_zero, eval_zero, wronskian_zero_left, degree_list_sum_le_of_forall_degree_le, div_eq_zero_iff, iterate_derivative_X_pow_eq_smul, WeierstrassCurve.Ο_zero, linearIndependent_powers_iff_aeval, modByMonic_zero, expand_eq_zero, Matrix.charmatrix_natCast, eraseLead_zero, eq_zero_of_degree_lt_of_eval_index_eq_zero, reflect_zero, Matrix.BlockTriangular.charmatrix, instIsCancelMulZeroOfIsCancelAdd, cardPowDegree_apply, dvd_derivative_iff, PowerSeries.weierstrassMod_zero_left, mul_self_modByMonic, eraseLead_C_mul_X_pow, ofFinsupp_smul, mirror_zero, RatFunc.num_eq_zero_iff, leadingCoeff_smul_of_smul_regular, eq_zero_of_natDegree_lt_card_of_eval_eq_zero, resultant_zero_left, eraseLead_X, trailingCoeff_zero, aroots_zero, Differential.mapCoeffs_X, RatFunc.zero_def, degree_smul_of_isRightRegular_leadingCoeff, derivativeFinsupp_map, minpoly.eq_zero, natSepDegree_mul_eq_iff, iterate_derivative_eq_zero_of_degree_lt, coeff_smul, support_smul, Splits.splits, eq_zero_of_hasseDeriv_eq_zero, degree_zero_le, eval_listSum, isNilpotent_monomial_iff, PolyEquivTensor.toFunAlgHom_apply_tmul_eq_smul, isNilpotent_iff, iterate_derivative_smul, natTrailingDegree_eq_support_min', card_support_eq_zero, FixedPoints.smul_polynomial, divX_zero, PolyEquivTensor.toFunBilinear_apply_apply, rootMultiplicity_eq_multiplicity, bernsteinPolynomial.eq_zero_of_lt, divX_C_mul_X_pow, WeierstrassCurve.Ξ¨_zero, WeierstrassCurve.Ξ¨Sq_zero, contentIdeal_eq_bot_iff, natDegree_smul_le, map_zero, coeffList_eq_nil, WeierstrassCurve.Affine.CoordinateRing.smul_basis_eq_zero, contentIdeal_zero, map_smul, mahlerMeasure_zero, eraseLead_C, degree_smul_le, cauchyBound_zero, divX_C, monomial_zero_right, divByMonic_zero, instIsLeftCancelMulZeroOfIsCancelAdd, Cubic.zero, isNilpotent_C_mul_pow_X_of_isNilpotent, IsCoprime.wronskian_eq_zero_iff, instNoZeroDivisors, Matrix.charmatrix_one, Matrix.coeff_det_one_add_X_smul_one, coeffList_zero, PolyEquivTensor.toFunBilinear_apply_eq_smul, isNilpotent_C_iff, hasseDeriv_C, coeff_list_sum, sum_zero_index, PowerSeries.IsWeierstrassDivisorAt.mod_zero, degree_map_eq_iff, toSubring_zero, smul_C, Chebyshev.U_neg_one, eq_zero_of_dvd_of_degree_lt, logMahlerMeasure_zero, toFinsupp_smul, hasseDeriv_apply_one, Lagrange.interpolate_empty, coeff_zero, derivativeFinsupp_one, isNilpotent_mul_X_iff, comp_zero, Cubic.of_d_eq_zero', RatFunc.mk_zero, isNilpotent_reflect_iff, derivative_C, eq_zero_of_dvd_of_natDegree_lt, support_eq_empty, aeval_zero, PowerSeries.IsWeierstrassDivisorAt.eq_zero_of_mul_eq, eval_smul, support_derivativeFinsupp_subset_range, mirror_eq_zero, gal_zero_isSolvable, derivative_zero, evalEval_zero, faithfulSMul, coe_zero, roots_eq_zero_iff_eq_zero_or_isRoot_eq_bot, map_eq_zero_iff, Monic.mul_natDegree_lt_iff, zero_scaleRoots, not_monic_zero_iff, PowerSeries.trunc_one_X, Monic.mul_left_eq_zero_iff, homogenize_zero, reverse_zero, map_eq_zero, matPolyEquiv_symm_X, Matrix.charmatrix_apply, scaleRoots_zero, smul_eval, Matrix.charmatrix_ofNat, smulCommClass, minpolyDiv_eq_zero, qsmul_eq_C_mul, eq_zero_of_infinite_isRoot, Cubic.toPoly_eq_zero_iff, ofFinsupp_eq_zero, isNilpotent_pow_X_mul_C_of_isNilpotent, evalEval_smul, mirror_smul, coeffs_zero, LaurentPolynomial.trunc_C_mul_T, derivative_natCast, comp_X_add_C_eq_zero_iff, natTrailingDegree_zero, hasseDeriv_X, PowerSeries.weierstrassMod_zero_right, monic_zero_iff_subsingleton', rootMultiplicity_zero, integralNormalization_zero, map_monic_eq_zero_iff, PowerSeries.weierstrassMod_zero, evalβ_smul, divX_one, isScalarTower_right, reflect_eq_zero_iff, splits_iff_splits, zero_modByMonic, matPolyEquiv_coeff_apply_aux_2, iterate_derivative_one, hilbertPoly_zero_right, degreeLTEquiv_eq_zero_iff_eq_zero, isUnit_leadingCoeff_mul_right_eq_zero_iff, smul_X_eq_monomial, annIdealGenerator_eq_zero_iff, matPolyEquiv_smul_one, trailingCoeff_eq_zero, isUnit_leadingCoeff_mul_left_eq_zero_iff, leadingCoeff_eq_zero, monic_zero_iff_subsingleton, isNilpotent_reverse_iff, PowerSeries.trunc_zero', hasseDeriv_eq_zero_of_lt_natDegree, Matrix.derivative_det_one_add_X_smul_aux, zero_notMem_multiset_map_X_add_C, transcendental_iff, Ideal.evalβ_C_mk_eq_zero, trailingDegree_eq_top, Matrix.charmatrix_diagonal, wronskian_zero_right, toFinsupp_zero, eq_zero_of_degree_lt_of_eval_finset_eq_zero, eval_smul', support_zero, erase_monomial, smeval_zero, derivative_one, supNorm_eq_zero_iff, smul_comp, polyEquivTensor_symm_apply_tmul_eq_smul, PowerSeries.isWeierstrassDivisionAt_zero, degree_eq_bot, degree_list_sum_le, Chebyshev.S_neg_one, resultant_zero_zero, derivativeFinsupp_C, derivativeFinsupp_X, roots_def, erase_zero, derivative_intCast, Mathlib.Tactic.ComputeDegree.coeff_smul, Matrix.isNilpotent_charpoly_sub_pow_of_isNilpotent
|
monomial π | CompOp | 135 mathmath: MvPolynomial.pUnitAlgEquiv_symm_monomial, support_monomial, eraseLead_monomial, smeval_monomial_mul, PolyEquivTensor.toFunBilinear_apply_eq_sum, monomial_eq_monomial_iff, opRingEquiv_op_monomial, natDegree_monomial_le, monomial_mem_lifts, sum_bernoulli, C_mul_X_eq_monomial, roots_monomial, monomial_one_one_eq_X, Splits.monomial, mirror_monomial, coeffs_monomial, ofFn_eq_sum_monomial, derivative_monomial, toFinsupp_monomial, coe_monomial, PolyEquivTensor.toFunAlgHom_apply_tmul, adjoin_monomial_eq_reesAlgebra, monomial_mul_C, X_pow_eq_monomial, self_sub_monomial_natDegree_leadingCoeff, evalβ_monomial, monomial_pow, toLaurent_C_mul_T, PolynomialModule.monomial_smul_single, X_pow_smul_rTensor_monomial, smul_monomial, map_monomial, matPolyEquiv_coeff_apply_aux_1, monomial_mem_adjoin_monomial, ofFinsupp_single, le_trailingDegree_monomial, C_mul_X_pow_eq_monomial, monomial_eq_zero_iff, natTrailingDegree_monomial, eval_monomial_one_add_sub, Derivation.mapCoeffs_monomial, addHom_ext'_iff, degree_monomial_le, coeff_monomial_of_ne, monomial_injective, polyEquivTensor_symm_apply_tmul, valuation_inv_monomial_eq_valuation_X_zpow, sum_monomial_index, sum_monomial_eq, C_mul_monomial, as_sum_range, monomial_mul_X, mapAlgHom_monomial, reesAlgebra.monomial_mem, coeff_monomial, Differential.mapCoeffs_monomial, mul_eq_sum_sum, monomial_zero_one, eraseLead_add_monomial_natDegree_leadingCoeff, monomial_one_eq_iff, coeff_monomial_zero_mul, coeff_mul_monomial_zero, AdjoinRoot.powerBasisAux'_repr_symm_apply, Bivariate.swap_monomial_monomial, PolynomialModule.equivPolynomial_single, supNorm_monomial, gaussNorm_monomial, expand_monomial, hasseDeriv_monomial, monomial_add, coeff_monomial_same, opRingEquiv_symm_monomial, toAddCircle_monomial_eq_smul_fourier, coe_basisMonomials, PowerSeries.trunc_apply, isNilpotent_monomial_iff, as_sum_range', natDegree_monomial, contentIdeal_monomial, bernoulli_def, lhom_ext'_iff, X_pow_mul_monomial, valuation_monomial_eq_valuation_X_pow, PolyEquivTensor.invFun_monomial, monomial_neg, monomial_zero_right, signVariations_monomial, monomial_mul_X_pow, X_mul_monomial, taylor_monomial, valuation_aeval_monomial_eq_valuation_pow, smeval_monomial, homogenize_monomial_of_lt, aroots_monomial, derivative_monomial_succ, PowerSeries.trunc_succ, monomial_one_right_eq_X_pow, MvPolynomial.optionEquivLeft_monomial, hasseDeriv_apply, addSubmonoid_closure_setOf_eq_monomial, sum_modByMonic_coeff, aeval_monomial, MvPolynomial.pUnitAlgEquiv_monomial, monomial_zero_left, succ_signVariations_X_sub_C_mul_monomial, as_sum_support, natTrailingDegree_monomial_le, PolynomialModule.monomial_smul_apply, logMahlerMeasure_monomial, rootSet_monomial, monomial_left_inj, natDegree_monomial_eq, leadingCoeff_monomial, card_support_le_one_iff_monomial, coeff_mul_monomial, LaurentPolynomial.trunc_C_mul_T, PolynomialModule.monomial_smul_lsingle, monomial_natDegree_leadingCoeff_eq_self, support_monomial', RatFunc.algebraMap_monomial, smul_X_eq_monomial, monomial_sub, coeff_monomial_succ, degree_monomial, isMonicOfDegree_monomial_one, trailingDegree_monomial, erase_monomial, monomial_comp, monomial_mul_monomial, coeff_monomial_mul, coeffList_monomial, content_monomial, homogenize_monomial, monomial_add_erase, eval_monomial
|
ofMultiset π | CompOp | 4 mathmath: rightInverse_ofMultiset_roots, roots_ofMultiset, ofMultiset_apply, ofMultiset_injective
|
pow π | CompOp | 2 mathmath: toFinsupp_pow, ofFinsupp_pow
|
repr π | CompOp | β |
semiring π | CompOp | 2226 mathmath: fderiv, mul_div_eq_iff_isRoot, PowerSeries.coeff_mul_eq_coeff_trunc_mul_truncβ, MvPolynomial.pUnitAlgEquiv_symm_monomial, PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_apply, rightInverse_ofMultiset_roots, support_monomial, units_coeff_zero_smul, NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply', isUnit_C_add_X_mul_iff, WeierstrassCurve.map_Οβ, natDegree_mul_X_pow, isMonicOfDegree_X_add_one, natDegree_mul_leadingCoeff_inv, degreeLT.addLinearEquiv_symm_apply_inr, taylor_eval, IsAdjoinRoot.repr_add_sub_repr_add_repr_mem_span, ker_mapRingHom, ZMod.irreducible_of_dvd_cyclotomic_of_natDegree, degree_pow_le_of_le, RatFunc.mk_def_of_ne, X_pow_mul_assoc_C, mem_aroots', separable_X_add_C, Lagrange.eval_iterate_derivative_eq_sum, mahlerMeasure_const, Ideal.Filtration.submodule_closure_single, eraseLead_monomial, PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply, RatFunc.ofFractionRing_mk', Derivation.apply_eval_eq, monic_X_pow, leadingCoeff_mul_X_pow, eq_X_sub_C_of_separable_of_root_eq, derivative_X_sq, coe_normUnit_of_ne_zero, Ideal.Filtration.submodule_eq_span_le_iff_stable_ge, separable_X_pow_sub_C_unit, smeval_monomial_mul, IntermediateField.aeval_gen_minpoly, RatFunc.mk_coe_def, splits_iff_exists_multiset, polynomialFunctions.eq_adjoin_X, ofFn_zero, toLaurent_eq_zero, mem_lifts_iff_mem_alg, roots_expand, taylorWithin_succ, MvPolynomial.pUnitAlgEquiv_apply, PolyEquivTensor.toFunBilinear_apply_eq_sum, algEquivCMulXAddC_apply, lcoeff_comp_mapAlgHom_eq, mul_divByMonic_eq_iff_isRoot, coe_taylorAlgHom, LaurentPolynomial.mk'_one_X_pow, cardPowDegree_zero, LinearMap.exists_monic_and_aeval_eq_zero, monic_X_sub_C, monomial_eq_monomial_iff, RatFunc.num_div, PolynomialModule.comp_single, coeff_X_pow_mul', coeff_derivative, degreeLT.instFreeSubtypeMemSubmodule, one_add_X_pow_sub_X_pow, AnalyticOn.aeval_polynomial, PowerBasis.exists_eq_aeval, FixedPoints.minpoly.irreducible, eq_cyclotomic_iff, MvPolynomial.support_finSuccEquiv, algebraMap_pi_eq_aeval, ker_evalRingHom, Monic.free_quotient, StandardEtalePair.inv_aeval_X_g, evalβ_intCastRingHom_X, IsPurelyInseparable.minpoly_eq', LaurentPolynomial.mk'_mul_T, expand_eq_sum, root_X_sub_C, Algebra.Norm.Transitivity.polyToMatrix_cornerAddX, polynomial_smul_apply', hasseDeriv_zero', continuous_aeval, X_pow_sub_C_splits_of_isPrimitiveRoot, Differential.implicitDeriv_C, Matrix.pow_eq_aeval_mod_charpoly, MvPolynomial.mem_image_support_coeff_finSuccEquiv, WeierstrassCurve.Affine.CoordinateRing.smul, resultant_X_add_C_right, pow_rootMultiplicity_dvd, derivWithin_aeval, AdjoinRoot.minpoly_root, X_pow_sub_C_eq_prod, derivative_intCast_mul, toMatrix_sylvesterMap', rootMultiplicity_eq_rootMultiplicity, eval_minpolyDiv_self, disjoint_ker_aeval_of_isCoprime, Ideal.mem_ofPolynomial, toAlgHom_taylorEquiv, PolynomialModule.smul_def, IsAdjoinRoot.mem_ker_map, aroots_smul_nonzero, mapAlgEquiv_id, expNegInvGlue.hasDerivAt_polynomial_eval_inv_mul, mem_reesAlgebra_iff_support, derivative_C_mul, aeval_algebraMap_apply_eq_algebraMap_eval, evalβ_minpolyDiv_self, support_trinomial, divX_X_pow, AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_symm_mk, KaehlerDifferential.polynomialEquiv_symm, Ideal.exists_mem_span_singleton_map_residueField_eq, iterate_derivative_zero, cyclotomic_six, rootMultiplicity_eq_natTrailingDegree, aeval_algebraMap_eq_zero_iff, card_rootSet_le_derivative, ConjRootClass.aeval_minpoly_iff, Ideal.exists_nonzero_mem_of_ne_bot, PowerSeries.coeff_trunc, WeierstrassCurve.map_Ο, contract_expand, derivative_mul, PowerSeries.trunc_mul_trunc, div_def, Chebyshev.one_sub_X_sq_mul_derivative_derivative_U_eq_poly_in_U, cyclotomic.irreducible, Cubic.of_a_eq_zero', WeierstrassCurve.Ξ¨Sq_even, C_inj, opRingEquiv_op_monomial, natDegree_monomial_le, prod_X_sub_C_nextCoeff, mem_roots_sub_C', Monic.leadingCoeff_C_mul, Ideal.mem_leadingCoeffNth_zero, leadingCoeff_quadratic, idealX_span, Multiset.prod_X_sub_X_eq_sum_esymm, PowerSeries.trunc_X_pow_self_mul, eraseLead_X_pow, coeffList_C_mul, support_C_mul_X, exists_partition_polynomial, Lagrange.derivative_nodal, nnqsmul_eq_C_mul, IsPrimitiveRoot.minpoly_dvd_pow_mod, PolynomialModule.map_smul, leadingCoeff_C_mul_of_isUnit, WeierstrassCurve.Affine.monic_polynomial, monomial_mem_lifts, aroots_X_sub_C, MvPolynomial.optionEquivLeft_C, taylor_mul, rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero, degree_quadratic_lt, WeierstrassCurve.Affine.CoordinateRing.basis_one, sum_bernoulli, cyclotomic_dvd_geom_sum_of_dvd, C_mul_X_eq_monomial, natSepDegree_pow, eval_det_add_X_smul, prod_multiset_X_sub_C_of_monic_of_roots_card_eq, mem_rootSet_of_injective, X_mem_lifts, not_isUnit_of_natDegree_pos, logMahlerMeasure_C_mul, C_1, aeval_map_algebraMap, degree_pow_le, evalβ_minpolyDiv_of_evalβ_eq_zero, charZero, IsMonicOfDegree.natDegree_sub_X_pow, WeierstrassCurve.Οβ_sq, instIsScalarTowerPolynomial_1, hasseDeriv_one', derivative_comp_one_sub_X, MvPolynomial.optionEquivLeft_X_some, PolynomialModule.comp_smul, monic_X_pow_add_C, monic_multisetProd_X_sub_C, derivative_pow_eq_zero, isCoprime_of_is_root_of_eval_derivative_ne_zero, PolyEquivTensor.right_inv, toPowerSeries_toMvPowerSeries, PolynomialModule.aeval_equivPolynomial, algEquivOfCompEqX_symm, leadingCoeff_det_X_one_add_C, MvPolynomial.pUnitAlgEquiv_symm_apply, quotientSpanXSubCAlgEquiv_symm_apply, degreeLT_mono, roots_monomial, coeff_zero_of_isScalarTower, X_pow_sub_C_irreducible_iff_of_odd, coeff_one_add_X_pow, zero_notMem_multiset_map_X_sub_C, card_roots_sub_C', rootMultiplicity_expand_pow, irreducible_of_monic, aeval_iterate_derivative_of_ge, eq_C_of_degree_eq_zero, derivative_expand, degree_pow, derivative_sum, isCoveringMapOn_eval, nextCoeffUp_C_eq_zero, X_pow_sub_C_irreducible_of_odd, aeval_fn_apply, derivative_pow_succ, coeff_pow_eq_ite_of_natDegree_le_of_le, MvPolynomial.natDegree_finSuccEquiv, WeierstrassCurve.map_Ξ¨, StandardEtalePresentation.toPresentation_algebra_smul, sum_smul_minpolyDiv_eq_X_pow, derivative_ofNat, monomial_one_one_eq_X, Ideal.quotient_map_C_eq_zero, natDegree_X_pow_sub_C, Splits.eval_derivative, irreducible_iff_roots_eq_zero_of_degree_le_three, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C, derivative_smul, isNilpotent_X_mul_iff, Splits.monomial, AlgebraicIndependent.polynomial_aeval_of_transcendental, roots_C_mul_X_pow, IsAdjoinRoot.adjoinRootAlgEquiv_symm_apply_eq_mk, IsDistinguishedAt.map_eq_X_pow, subalgebraNontrivial, dickson_two_zero, LaurentPolynomial.mk'_one_X, RatFunc.laurent_algebraMap, iterate_derivative_eq_factorial_smul_sum, iterate_derivative_X_add_pow, PowerBasis.quotientEquivQuotientMinpolyMap_apply, WeierstrassCurve.Ξ¨Sq_odd, Chebyshev.S_eq_U_comp_half_mul_X, pUnitAlgEquiv_symm_toPowerSeries, evalβ_X_pow, degree_C_mul_of_isUnit, aroots_quadratic_eq_pair_iff_of_ne_zero', derivative_X, sumIDeriv_map, degree_mul_leadingCoeff_inv, AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin, eq_prod_roots_of_splits, eq_prod_roots_of_monic_of_splits_id, WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_C, mirror_monomial, WeierstrassCurve.Affine.Y_sub_negPolynomial, Module.AEval.of_symm_smul, dvd_iterate_derivative_pow, coeffs_monomial, KaehlerDifferential.polynomialEquiv_D, MvPolynomial.optionEquivLeft_apply, minpoly_algHom_toLinearMap, ofFn_eq_sum_monomial, hilbertPoly_smul, MvPolynomial.totalDegree_coeff_finSuccEquiv_add_le, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_eqβ, prime_C_iff, AdjoinRoot.mk_surjective, Lagrange.interpolate_eq_nodalWeight_mul_nodal_div_X_sub_C, pow_comp, abc, finrank_quotient_span_eq_natDegree', cyclotomic_expand_eq_cyclotomic_mul, LinearMap.charpoly_nilpotent_tfae, WeierstrassCurve.Affine.CoordinateRing.coe_basis, natSepDegree_X_sub_C_pow, isMonicOfDegree_two_iff', not_isRoot_C, Multiset.prod_X_add_C_coeff, exists_partition_polynomial_aux, natDegree_C_add, Splits.eval_root_derivative, Monic.eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one, C_mul', eraseLead_add_C_mul_X_pow, matPolyEquiv_map_smul, RatFunc.laurent_div, minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C, isMonicOfDegree_X_sub_one, degreeLT.basis_val, reverse_mul_X_pow, derivative_monomial, ConjRootClass.minpoly.map_eq_prod, not_dvd_of_degree_lt, aeval_sumIDeriv, WeierstrassCurve.Affine.map_polynomialY, Monic.natDegree_pow, sumIDeriv_C, Chebyshev.T_derivative_eq_U, Subalgebra.aeval_coe, matPolyEquiv_diagonal_X, coeff_taylor_natDegree, roots_C_mul, Ideal.Filtration.mem_submodule, coeff_divByMonic_X_sub_C_rec, gal_X_pow_isSolvable, Subfield.splits_bot, monic_X_pow_add, RatFunc.liftOn_ofFractionRing_mk, leadingCoeff_X_pow_add_C, eval_C, Chebyshev.iterate_derivative_T_eval_one_recurrence, smeval_X_pow, Matrix.charmatrix_apply_eq, toFinsupp_monomial, Lagrange.nodal_insert_eq_nodal, mapAlgHom_eq_evalβAlgHom'_CAlgHom, coe_monomial, rootMultiplicity_sub_one_le_derivative_rootMultiplicity, PolyEquivTensor.toFunAlgHom_apply_tmul, Matrix.charpoly_natCast, eval_divByMonic_eq_trailingCoeff_comp, algebraMap_apply, evalEval_finset_sum, PowerBasis.equivAdjoinSimple_symm_aeval, adjoin_monomial_eq_reesAlgebra, MvPolynomial.optionEquivRight_C, monomial_mul_C, Monic.geom_sum', IsPrimitive.isUnit_iff_isUnit_map_of_injective, X_pow_eq_monomial, Bivariate.Polynomial.Bivariate.pderiv_one_equivMvPolynomial, X_pow_sub_C_irreducible_iff_forall_prime_of_odd, not_isUnit_of_degree_pos_of_isReduced, trunc_toLaurent, toAddCircle_X_pow_eq_fourier, as_sum_range_C_mul_X_pow', Matrix.derivative_det_one_add_X_smul, integralNormalization_C, Splits.mem_lift_of_roots_mem_range, rootMultiplicity_X_sub_C_pow, resultant_X_sub_C_right, differentiableOn_aeval, mem_iff_eq_smul_annIdealGenerator, MvPolynomial.degreeOf_coeff_finSuccEquiv, derivative_rootMultiplicity_of_root, transcendental_iff_injective, taylor_injective, iterate_derivative_mul_X, evalβRingHom_evalβRingHom, isUnit_map, update_eq_add_sub_coeff, monic_finprod_X_sub_C, degree_C_mul_of_mul_ne_zero, Ideal.jacobson_bot_polynomial_le_sInf_map_maximal, IsCyclotomicExtension.aeval_zeta, Real.Polynomial.isRoot_cos_pi_div_five, coe_C, instIsDomainOfIsCancelAdd, WeierstrassCurve.Affine.C_addPolynomial, sumIDeriv_eq_self_add, self_sub_monomial_natDegree_leadingCoeff, bernoulli_generating_function, natDegree_finset_prod_X_sub_C_eq_card, support_C_mul_X', prod_cyclotomic_eq_X_pow_sub_one, iterate_derivative_X, MvPolynomial.nonempty_support_finSuccEquiv, natDegree_sum_le, evalβ_monomial, Matrix.charpoly_mul_comm_of_le, Module.AEval'.X_smul_of, AdjoinRoot.smul_mk, Splits.eval_derivative_eq_eval_mul_sum, AdjoinRoot.quotEquivQuotMap_symm_apply_mk, coe_compRingHom_apply, WeierstrassCurve.Affine.irreducible_polynomial, pow_rootMultiplicity_not_dvd, divByMonic_add_X_sub_C_mul_derivative_divByMonic_eq_derivative, AdjoinRoot.evalEval_apply, derivative'_apply, constantCoeff_apply, mem_support_derivative, aeval_X_pow, PowerSeries.eq_shift_mul_X_pow_add_trunc, monomial_pow, coeff_mul_X_pow, evalEval_intCast, Bivariate.aveal_eq_map_swap, le_trailingDegree_C, WeierstrassCurve.Affine.polynomial_eq, evalβ_finset_sum, WeierstrassCurve.preΞ¨_odd, toLaurent_C_mul_T, resultant_X_pow_right, card_roots_le_derivative, aevalTower_algebraMap, rootsExpandPowEquivRoots_apply, Bivariate.swap_apply, derivative_eval, WeierstrassCurve.Ξ¨_one, LindemannWeierstrass.exp_polynomial_approx, map_expand, PolynomialModule.monomial_smul_single, Ideal.injective_quotient_le_comap_map, C_eq_zero, dvd_comp_X_add_C_iff, separable_X_pow_sub_C, span_singleton_annIdealGenerator, Monic.eq_X_pow_iff_natDegree_le_natTrailingDegree, dvd_comp_C_mul_X_add_C_iff, algEquivCMulXAddC_symm_eq, X_pow_smul_rTensor_monomial, X_pow_sub_one_splits, WeierstrassCurve.Affine.natDegree_polynomial, coeff_C_ne_zero, isMonicOfDegree_add_add_two, degree_X_pow_add_C, Matrix.det_one_add_smul, IsUnitTrinomial.irreducible_of_isCoprime, smul_monomial, Monic.comp_X_sub_C, WeierstrassCurve.Affine.CoordinateRing.instIsScalarTowerPolynomial, leadingCoeff_smul_integralNormalization, eval_pow, MvPolynomial.evalβ_const_pUnitAlgEquiv_symm, MvPolynomial.eval_comp_toMvPolynomial, degree_X_sub_C, iterate_derivative_X_sub_pow, MvPolynomial.support_finSuccEquiv_nonempty, support_trinomial', C_0, isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top, PowerSeries.degree_trunc_lt, irreducible_of_eisenstein_criterion, PowerSeries.IsWeierstrassFactorization.isWeierstrassDivision, expand_eq_comp_X_pow, FirstOrder.Field.lift_genericMonicPoly, exists_finset_of_splits, Chebyshev.T_two, Submodule.IsPrincipal.contentIdeal_le_span_iff_dvd, IntermediateField.aeval_coe, WeierstrassCurve.Ξ¨Sq_ofNat, Matrix.charpoly_of_upperTriangular, Monic.not_dvd_of_natDegree_lt, irreducible_mul_leadingCoeff_inv, IsSepClosed.roots_eq_zero_iff, MvPolynomial.degree_optionEquivLeft, aeval_one, Module.AEval.instIsScalarTowerOrigPolynomial, gal_X_pow_sub_C_isSolvable, Lagrange.interpolate_eq_sum, Module.AEval.C_smul, sum_C_index, Matrix.charmatrix_apply_ne, aeval_eq_zero_of_mem_rootSet, degreeLT.addLinearEquiv_castAdd, KaehlerDifferential.polynomialEquiv_comp_D, coeff_X_pow_mul, IsLocalization.integerNormalization_map_to_map, FiniteField.roots_X_pow_card_sub_X, Algebra.discr_powerBasis_eq_norm, natTrailingDegree_C, PowerBasis.quotientEquivQuotientMinpolyMap_apply_mk, X_mul_C, algebraMap_def, Derivation.mapCoeffs_C, coeff_C_mul_X, leadingCoeff_cubic, eval_X_pow, map_monomial, expand_one, resultant_C_zero_right, natDegree_eq_one, aeval_subalgebra_coe, minpoly.sub_algebraMap, WeierstrassCurve.Ο_three, AdjoinRoot.mk_eq_mk, X_pow_mul_assoc, matPolyEquiv_coeff_apply_aux_1, leadingCoeffHom_apply, degreeLT.addLinearEquiv_apply_fst, C_eq_natCast, isConjRoot_iff_aeval_eq_zero, coeff_X_pow, RatFunc.mk_eq_mk', derivative_X_sub_C_sq, Matrix.charpoly_sub_scalar, aeval_X_left_apply, smul_eq_C_mul, FiniteField.instIsSplittingFieldExtensionHSubPolynomialHPowNatXCard, opRingEquiv_op_C, WeierstrassCurve.baseChange_Οβ, Chebyshev.U_two, C_eq_intCast, smeval.linearMap_apply, degree_C_lt_degree_C_mul_X, aroots_C_mul, eval_derivative_of_splits, isUnit_iff, Splits.X_pow, roots_X_pow_char_pow_sub_C_pow, coeff_mapAlgHom_apply, Multiset.prod_X_sub_C_dvd_iff_le_roots, divRadical_dvd_derivative, aeval_prod_apply, leadingCoeff_mul_prod_normalizedFactors, Module.AEval'.of_symm_X_smul, squarefree_cyclotomic, aeval_add_of_sq_eq_zero, monomial_mem_adjoin_monomial, Matrix.IsHermitian.charpoly_cfc_eq, mem_span_C_X_sub_C_X_sub_C_iff_eval_eval_eq_zero, derivativeFinsupp_apply_toFun, Chebyshev.aeval_T, aeval_comp, deriv_aeval, Chebyshev.S_sq_add_S_sq, nextCoeff_C_mul_X_add_C, monic_mapAlg_iff, matPolyEquiv_symm_apply_coeff, ofFinsupp_single, splits_pow, toLaurent_injective, le_trailingDegree_monomial, X_pow_sub_one_dvd_prod_cyclotomic, prod_multiset_root_eq_finset_root, dvd_C_mul, iterate_derivative_derivative_mul_X_sq, Monic.irreducible_iff_lt_natDegree_lt, toMvPolynomial_eq_rename_comp, WeierstrassCurve.Affine.baseChange_negPolynomial, Derivation.comp_aeval_eq, X_pow_sub_C_separable_iff, IsPurelyInseparable.minpoly_eq, Ideal.polynomial_not_isField, nextCoeff_mul_C, coeff_X_sub_C_mul, WeierstrassCurve.Affine.CoordinateRing.mk_Ο, Cubic.of_a_eq_zero, comp_C_mul_X_eq_zero_iff, modByMonic_eq_zero_iff_quotient_eq_zero, evalEval_sum, comap_taylorEquiv_degreeLT, ofReal_eval, degree_quadratic, evalEval_X, PowerSeries.trunc_trunc_mul_trunc, MvPolynomial.transcendental_polynomial_aeval_X_iff, monic_X_pow_sub_C, rootsExpandEquivRoots_apply, leadingCoeff_linear, aeval_prod, rootMultiplicity_eq_natFind_of_ne_zero, isMonicOfDegree_two_iff, C_mul_X_pow_eq_monomial, nextCoeff_X_add_C, StandardEtalePair.equivMvPolynomialQuotient_symm_apply, PowerSeries.trunc_mul_C, eq_X_add_C_of_degree_le_one, taylor_zero', MvPolynomial.eval_eq_eval_mv_eval', isUnit_iff', WeierstrassCurve.preΞ¨'_even, evalEvalRingHom_eq, expand_C, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply_mk, logMahlerMeasure_X_sub_C, C_mem_lifts, aevalTower_toAlgHom, monomial_eq_zero_iff, card_roots_toFinset_le_card_roots_derivative_diff_roots_succ, MvPolynomial.optionEquivLeft_X_none, IsAdjoinRootMonic.map_modByMonic, MvPolynomial.algebraicIndependent_polynomial_aeval_X, natDegree_mul_leadingCoeff_self_inv, CAlgHom_apply, trailingDegree_C_mul_X_pow, X_pow_sub_one_eq_prod, toAddCircle.integrable, prod_multiset_X_sub_C_dvd, degree_cubic_lt, AdjoinRoot.mul_div_root_cancel, eq_X_add_C_of_natDegree_le_one, minpoly.natSepDegree_eq_one_iff_eq_X_sub_C_pow, degree_C, Cubic.of_b_eq_zero, mkDerivation_one_eq_derivative', natTrailingDegree_mul_X_pow, derivative_X_add_C, hermite_succ, Real.fibRec_charPoly_eq, instCharP, Matrix.charpoly_zero, PolyEquivTensor.toFunLinear_mul_tmul_mul, hermite_eq_iterate, ofFinsupp_algebraMap, aeval_pi_apply, hasseDeriv_comp, IsAdjoinRoot.map_repr, aevalTower_comp_algebraMap, WeierstrassCurve.Affine.CoordinateRing.C_addPolynomial, AdjoinRoot.aeval_eq_of_algebra, support_binomial', cyclotomic_eq_prod_X_sub_primitiveRoots, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_add_eq, roots_pow, X_add_C_scaleRoots, resultant_C_right, splits_C, Splits.comp_X_sub_C, iterate_derivative_natCast_mul, WeierstrassCurve.Ξ¨_ofNat, evalβ_sum, aevalTower_X, AdjoinRoot.mk_leftInverse, natDegree_C_mul_X, differentiable_aeval, natTrailingDegree_monomial, comp_C, coeff_mul_X_sub_C, bernsteinPolynomial.iterate_derivative_at_1_eq_zero_of_lt, finrank_quotient_span_eq_natDegree, eval_monomial_one_add_sub, RatFunc.numDenom_div, roots_expand_map_frobenius, map_pow, gal_X_pow_sub_one_isSolvable, natDegree_X_add_C, map_taylor, LieAlgebra.engel_isBot_of_isMin.lieCharpoly_map_eval, aeval_X_left, map_under_lt_comap_of_weaklyQuasiFiniteAt, MvPolynomial.finSuccEquiv_coeff_coeff, support_C, Derivation.mapCoeffs_monomial, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C', roots_expand_image_frobenius, degreeLT.addLinearEquiv_apply_snd, natSepDegree_C_mul_X_sub_C_pow, IsPrimitive.irreducible_iff_irreducible_map_fraction_map, height_map_C, RatFunc.num_C, WeierstrassCurve.Ξ¨_neg, minpoly.dvd_iff, X_sub_C_mul_divByMonic_eq_sub_modByMonic, IsNilpotent.charpoly_eq_X_pow_finrank, addHom_ext'_iff, natDegree_sum_eq_of_disjoint, RatFunc.smul_eq_C_mul, roots_C_mul_X_sub_C_of_IsUnit, PowerSeries.trunc_X_of, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk, evalEval_multiset_prod, derivative_X_pow_succ, degree_X_pow_le, eq_C_of_natDegree_le_zero, monic_X_add_C, logMahlerMeasure_X_add_C, aevalTower_C, modByMonic_eq_zero_iff_dvd, WeierstrassCurve.Affine.addPolynomial_slope, cfc_map_polynomial, coeff_C_mul, idealSpan_range_update_divByMonic, degree_monomial_le, rootMultiplicity_eq_nat_find_of_nonzero, roots_quadratic_eq_pair_iff_of_ne_zero, coeff_monomial_of_ne, derivative_X_sub_C_pow, cyclotomic_mul_prime_dvd_eq_pow, natDegree_C_mul_eq_of_mul_eq_one, IsMonicOfDegree.exists_natDegree_lt, eraseLead_C_mul_X, natDegree_C, hilbertPoly_succ, ker_constantCoeff, X_pow_sub_C_irreducible_iff_of_prime_pow, Lagrange.basis_eq_prod_sub_inv_mul_nodal_div, WeierstrassCurve.Affine.map_negPolynomial, IsAdjoinRoot.map_X, Monic.eq_X_pow_iff_natTrailingDegree_eq_natDegree, toLaurent_comp_C, polynomialFunctions.starClosure_eq_adjoin_X, IsRoot.mul_div_eq, sum_C_mul_X_pow_eq, LinearMap.pow_eq_aeval_mod_charpoly, not_isUnit_of_degree_pos, PowerBasis.liftEquiv_symm_apply, Module.AEval'.X_pow_smul_of, as_sum_support_C_mul_X_pow, toFinsupp_X_pow, derivWithin, Chebyshev.one_sub_X_sq_mul_derivative_T_eq_poly_in_T, degree_quadratic_le, eq_quadratic_of_degree_le_two, WeierstrassCurve.Ο_one, adjSylvester_comp_sylveserMap, exists_iterate_derivative_eq_factorial_smul, divX_eq_zero_iff, rootsExpandPowToRoots_apply, reflect_one, MulSemiringAction.charpoly_eq_prod_smul, monomial_injective, taylor_eq_zero, AdjoinRoot.mk_eq_zero, card_support_eq, reflect_monomial, leadingCoeff_pow_X_add_C, PowerBasis.equivAdjoinSimple_aeval, rank_polynomial_polynomial, cauchyBound_C, mem_lifts, RatFunc.laurentAux_div, traceForm_dualSubmodule_adjoin, X_pow_sub_X_sub_one_irreducible, polyEquivTensor_symm_apply_tmul, roots_C_mul_X_add_C, natDegree_C_mul_le, divX_hom_toFun, LinearMap.charpoly_eq_X_pow_iff, sum_comp, leadingCoeff_X_pow_sub_C, LaurentPolynomial.mk'_eq, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some, AdjoinRoot.span_maximal_of_irreducible, WeierstrassCurve.baseChange_Ο, AdjoinRoot.quotEquivQuotMap_apply, degreeLT.instFiniteSubtypeMemSubmodule, IsAdjoinRootMonic.modByMonicHom_map, derivativeFinsupp_apply_apply, Bivariate.equivMvPolynomial_symm_X_0, sup_aeval_range_eq_top_of_isCoprime, minpoly.eq_X_sub_C_of_algebraMap_inj, taylor_apply, charP, natDegree_C_mul_of_mul_ne_zero, eval_derivative_eq_eval_mul_sum_of_splits, WeierstrassCurve.Affine.C_addPolynomial_slope, iterate_derivative_comp_one_sub_X, Splits.eq_prod_roots, evalEvalRingHom_apply, spectralNorm.spectralNorm_pow_natDegree_eq_prod_roots, instIsScalarTowerPolynomial, Monic.not_dvd_of_degree_lt, notMem_nonZeroDivisors_iff, degree_derivative_lt, div_wf_lemma, Matrix.charmatrix_fromBlocks, derivative_natCast_mul, mapAlgEquiv_comp, eq_X_add_C_of_degree_eq_one, prod_cyclotomic'_eq_X_pow_sub_one, fderiv_aeval, Splits.eval_derivative_div_eval_of_ne_zero, sup_ker_aeval_eq_ker_aeval_mul_of_coprime, mahlerMeasure_C_mul_X_add_C, IsAlgebraic.exists_nonzero_coeff_and_aeval_eq_zero, Module.End.aeval_apply_of_hasEigenvector, PowerBasis.mem_span_pow', KummerDedekind.emultiplicity_factors_map_eq_emultiplicity, eq_C_of_natDegree_eq_zero, evalβ_C_X, sum_monomial_index, derivativeFinsupp_derivative, lifts_iff_ringHom_rangeS, smeval_C, Algebra.adjoin_singleton_eq_range_aeval, mem_span_C_coeff, WeierstrassCurve.Affine.CoordinateRing.norm_smul_basis, isCoprime_expand, IsCyclotomicExtension.isSplittingField_X_pow_sub_one, X_mul_divX_add, card_support_binomial, sum_monomial_eq, separable_C_mul_X_pow_add_C_mul_X_add_C', PowerSeries.trunc_trunc_mul, WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis, Splits.comp_X_add_C, Monic.isUnit_iff, degree_derivative_eq, C_mul_monomial, natDegree_hasseDeriv_le, evalEval_prod, MvPolynomial.optionEquivLeft_coeff_coeff, monic_C_mul_of_mul_leadingCoeff_eq_one, separable_X_pow_sub_C', Matrix.charpoly.optionEquivLeft_symm_univ_isHomogeneous, fact_irreducible_factor, IsCyclotomicExtension.splits_X_pow_sub_one, transcendental_aeval_iff, coeff_pow_mul_natDegree, Splits.aeval_eq_prod_aroots, as_sum_range, toLaurent_apply, not_isField, expand_inj, PolynomialModule.isScalarTower', natDegree_mul_C_eq_of_mul_eq_one, content_C_mul, Splits.eq_X_sub_C_of_single_root, coeff_det_X_add_C_card, isUnit_of_coeff_isUnit_isNilpotent, not_isUnit_of_natDegree_pos_of_isReduced, associated_of_dvd_of_natDegree_le, quotientSpanXSubCAlgEquiv_mk, Cubic.of_c_eq_zero', cyclotomic_prime_pow_eq_geom_sum, smeval_X_pow_mul, evalRingHom_mapMatrix_comp_polyToMatrix, NumberField.Ideal.liesOver_primesOverSpanEquivMonicFactorsMod_symm, aeval_X_left_eq_map, Lagrange.X_sub_C_dvd_nodal, det_taylorLinearEquiv_toLinearMap, roots_X_sub_C, isUnit_C, PowerSeries.smul_weierstrassMod, expand_expand, WeierstrassCurve.C_Ξ¨βSq, natDegree_quadratic_le, Bivariate.swap_Y, rootSet_C_mul_X_pow, natDegree_sum_le_of_forall_le, monomial_mul_X, rootSet_derivative_subset_convexHull_rootSet, mapAlgHom_monomial, Chebyshev.iterate_derivative_T_eval_zero_recurrence, iterate_derivative_X_pow_eq_natCast_mul, AnalyticWithinAt.aeval_polynomial, le_rootMultiplicity_iff, natDegree_taylor, degree_taylor, lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors, annIdealGenerator_mem, support_C_subset, hasFDerivAt, Cubic.of_b_eq_zero', WeierstrassCurve.Affine.derivative_addPolynomial_slope, support_C_mul_X_pow', aeval_apply_smul_mem_of_le_comap, eq_C_content_mul_primPart, degree_sum_le, C'_mem_lifts, rootMultiplicity_mul_X_sub_C_pow, Module.AEval.isTorsion_of_finiteDimensional, Ideal.mem_leadingCoeff, degreeLT.addLinearEquiv_apply, minpoly.ker_aeval_eq_span_minpoly, Chebyshev.aeval_S, mem_annIdeal_iff_aeval_eq_zero, card_support_eq', valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X, instIsNoetherianRingSubtypePolynomialMemSubalgebraReesAlgebra, C_eq_algebraMap, mapAlg_eq_map, separable_def', IsPrimitiveRoot.minpoly_dvd_expand, eval_unique, derivative_of_natDegree_zero, Finset.prod_X_add_C_coeff, Bivariate.equivMvPolynomial_symm_C, Matrix.charpoly_one, divX_mul_X_add, Subfield.roots_X_pow_char_sub_X_bot, aeval_eq_smeval, toFinsuppIsoLinear_symm_apply_toFinsupp, natSepDegree_X_pow_char_pow_sub_C, LaurentPolynomial.algebraMap_X_pow, homogenize_X_pow, evalEval_sub, minpoly.isRadical, IsPrimitive.Int.irreducible_iff_irreducible_map_cast, coeffList_C, Splits.taylor, Matrix.det_one_add_X_smul, Algebra.adjoin_mem_exists_aeval, coe_polyEquivTensor'_symm, FiniteField.isSplittingField_of_nat_card_eq, reesAlgebra.monomial_mem, lt_rootMultiplicity_iff_isRoot_iterate_derivative, Ideal.Filtration.inf_submodule, roots_expand_image_frobenius_subset, PowerSeries.derivativeFun_coe, comp_eq_zero_iff, isNilpotent_aeval_sub_of_isNilpotent_sub, Module.End.IsSemisimple.aeval, coeff_monomial, RatFunc.smul_eq_C_smul, Differential.mapCoeffs_monomial, MvPolynomial.support_coeff_finSuccEquiv, Module.AEval.X_pow_smul_of, minpoly.aeval, degree_X_pow_sub_C, taylor_coeff_zero, mul_eq_sum_sum, coe_polyEquivTensor', natDegree_X_pow_add_C, instExpChar, isUnit_iff_coeff_isUnit_isNilpotent, divX_C_mul, PowerSeries.eq_X_pow_mul_shift_add_trunc, iterate_derivative_C, degree_mul_leadingCoeff_self_inv, PowerSeries.trunc_trunc_of_le, mahlerMeasure_X_add_C, WeierstrassCurve.Ο_even, coeff_pow_of_natDegree_le, taylor_X_pow, reverse_X_pow_mul, Matrix.GeneralLinearGroup.fixpointPolynomial_aeval_eq_zero_iff, LaurentPolynomial.algebraMap_eq_toLaurent, eq_C_coeff_zero_iff_natDegree_eq_zero, Differential.mapCoeffs_C, IsUnitTrinomial.not_isUnit, comp_C_mul_X_coeff, Ideal.mem_leadingCoeffNth, cyclotomic_prime_pow_mul_X_pow_sub_one, int_evalβ_eq, gal_C_isSolvable, evalRingHom_mapMatrix_comp_compRingEquiv, resultant_X_sub_C_pow_left, bernsteinPolynomial.variance, toFn_zero, toLaurent_X_pow, ofFn_zero', RatFunc.instIsScalarTowerOfIsDomainOfPolynomial, derivative_C_mul_X, Bivariate.swap_X, AdjoinRoot.lift_mk, eval_iterate_derivative_rootMultiplicity, lcoeff_apply, iterate_derivative_derivative_mul_X, Chebyshev.add_one_mul_self_mul_T_eq_poly_in_T, WeierstrassCurve.Affine.CoordinateRing.map_mk, Splits.X_add_C, bernoulli_eq_sub_sum, degree_C_lt, leadingCoeff_pow', padic_polynomial_dist, aeval_conj, nextCoeff_C_eq_zero, iterate_derivative_eq_zero, hasseDeriv_coeff, degree_C_mul_X_pow_le, separable_prod_X_sub_C_iff', le_trailingDegree_C_mul_X_pow, map_mapRingHom_evalEval, algEquivAevalNegX_symm_apply, derivative_rootMultiplicity_of_root_of_mem_nonZeroDivisors, AdjoinRoot.root_isInv, monomial_zero_one, FiniteField.splits_X_pow_nat_card_sub_X, hasseDeriv_mul, PowerSeries.trunc_one_left, IsAdjoinRoot.adjoinRootAlgEquiv_apply_eq_map, coeff_mul_C, hermite_eq_deriv_gaussian', aeval_smul, rootMultiplicity_C, eq_prod_roots_of_splits_id, eraseLead_add_monomial_natDegree_leadingCoeff, RatFunc.laurentAux_algebraMap, IsAdjoinRoot.repr_zero_mem_span, coeff_C, AdjoinRoot.modByMonicHom_mk, Ideal.Filtration.submodule_span_single, natDegree_X_sub_C, WeierstrassCurve.Affine.CoordinateRing.mk_Ο, Bivariate.equivMvPolynomial_symm_X_1, iterate_derivative_X_pow_eq_smul, WeierstrassCurve.Ο_zero, Matrix.matPolyEquiv_charmatrix, natDegree_C_mul, PowerBasis.mem_span_pow, card_support_eq_three, aeval_def, Chebyshev.derivative_U_eval_one, aeval_mul, monomial_one_eq_iff, resultant_X_sub_C_pow_right, StandardEtalePresentation.toSubmersivePresentation_jacobian, smeval_C_mul, IsAlgClosed.exists_aeval_eq_zero_of_injective, X_sub_C_dvd_sub_C_eval, expand_eq_zero, degreeLT.addLinearEquiv_apply', WeierstrassCurve.Ξ¨_three, differentiableAt_aeval, WeierstrassCurve.Affine.Y_sub_polynomialY, hasseDeriv_zero, prime_X_sub_C, coeff_monomial_zero_mul, hilbertPoly_X_pow_succ, Monic.mem_nonZeroDivisors, Lagrange.iterate_derivative_interpolate, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, taylorAlgHom_apply, pow_sub_dvd_iterate_derivative_pow, hasFDerivAt_aeval, associated_of_dvd_of_degree_eq, IsAdjoinRoot.lift_map, C_sub, algEquivOfCompEqX_symm_apply, roots_X_pow_char_sub_C_pow, finset_sum_coeff, mem_nonZeroDivisors_iff, mem_nonZeroDivisors_of_trailingCoeff, aeval_eq_prod_aroots_sub_of_monic_of_splits, MvPolynomial.mem_support_coeff_optionEquivLeft, coeff_sum, Bivariate.swap_C_C, AdjoinRoot.liftAlgHom_mk, natDegree_derivative_le, RatFunc.faithfulSMul, LinearMap.aeval_eq_aeval_mod_charpoly, deriv_gaussian_eq_hermite_mul_gaussian, LinearMap.hasEigenvalue_zero_tfae, iterate_derivative_eq_sum, PolynomialModule.smul_apply, algEquivAevalXAddC_symm_apply, MvPolynomial.aeval_toMvPolynomial, Chebyshev.iterate_derivative_U_eval_zero_recurrence, resultant_pow_right, isMaximal_comap_C_of_isJacobsonRing, nextCoeff_X_sub_C, natDegree_C_mul_X_pow, AdjoinRoot.coe_mkβ, evalEval_pow, PolyEquivTensor.invFun_add, dvd_mul_leadingCoeff_inv, RatFunc.algebraMap_C, C_mul_X_pow_eq_self, leadingCoeff_X_pow, AnalyticAt.aeval_polynomial, degree_X_sub_C_le, PowerSeries.trunc_C, Monic.mem_rootSet, cardPowDegree_apply, spectrum.map_polynomial_aeval_of_nonempty, AdjoinRoot.Minpoly.coe_toAdjoin_mk_X, sumIDeriv_apply, sylvesterDeriv_updateRow, degree_C_mul_X_le, mul_X_pow_comp, dvd_derivative_iff, coeff_mul_monomial_zero, roots_ofMultiset, expand_zero, cyclotomic.dvd_X_pow_sub_one, eraseLead_C_mul_X_pow, roots_expand_pow_map_iterateFrobenius_le, Monic.natSepDegree_eq_one_iff, resultant_taylor, trailingDegree_C, leadingCoeff_sum_of_degree_eq, Ideal.is_fg_degreeLE, X_pow_sub_C_irreducible_of_prime, roots_multiset_prod_X_sub_C, homogenize_finsetSum, PowerBasis.equivOfMinpoly_aeval, degreeLT.addLinearEquiv_symm_apply_inl, MvPolynomial.aeval_toPolynomialAdjoinImageCompl_eq_zero, degreeLT.addLinearEquiv_symm_apply_inr_basis, natDegree_hasseDeriv, homogenize_C_mul, AdjoinRoot.powerBasisAux'_repr_symm_apply, Bivariate.swap_monomial_monomial, rootMultiplicity_expand, bernoulli_comp_one_add_X, X_pow_dvd_iff, contract_C, Matrix.charpoly_fin_two, evalβ_mul_C', eval_derivative_div_eval_of_ne_zero_of_splits, Chebyshev.one_sub_X_sq_mul_iterate_derivative_U_eval, separable_prod_X_sub_C_iff, MvPolynomial.totalDegree_coeff_optionEquivLeft_add_le, resultant_C_left, LinearMap.charpoly_constantCoeff_eq_zero_iff, PolynomialModule.equivPolynomial_single, natDegree_mul_C_of_isUnit, dickson_add_two, toFn_comp_ofFn_eq_id, AdjoinRoot.quotEquivQuotMap_apply_mk, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply, irreducible_of_degree_eq_one_of_isRelPrime_coeff, exists_eq_pow_rootMultiplicity_mul_and_not_dvd, supNorm_monomial, Bivariate.swap_map_C, derivative_comp, Monic.eq_X_add_C, transcendental_iff_ker_eq_bot, WeierstrassCurve.Affine.CoordinateRing.mk_Ξ¨_sq, mapRingHom_comp_C, eq_C_of_degree_le_zero, mem_nonZeroDivisors_of_leadingCoeff, gaussNorm_monomial, expand_X, contentIdeal_C, taylor_taylor, WeierstrassCurve.Ξ¦_ofNat, exists_approx_polynomial, eval_C_X_evalβ_map_C_X, minpoly.isIntegrallyClosed_dvd_iff, expand_monomial, PolynomialModule.smul_single_apply, supNorm_C, Monic.irreducible_iff_natDegree, eval_finset_sum, matPolyEquiv_map_C, card_roots_X_pow_sub_C, WeierstrassCurve.baseChange_Ξ¨, Algebra.Norm.Transitivity.eval_zero_comp_det, instIsTorsionFree, pow_scaleRoots_of_isReduced, mul_scaleRoots, X_pow_sub_one_separable_iff, WeierstrassCurve.Affine.map_polynomial, derivative_sq, leadingCoeff_C_mul_X_pow, mem_roots_sub_C, hermite_eq_deriv_gaussian, Monic.finite_quotient, WeierstrassCurve.Ξ¦_three, MvPolynomial.optionEquivLeft_coeff_some_coeff_none, isMaximal_comap_C_of_isMaximal, not_isUnit_X_add_C, roots_smul_nonzero, degree_cubic, LinearMap.isNilpotent_iff_charpoly, natSepDegree_C_mul, Algebra.adjoin_eq_exists_aeval, WeierstrassCurve.Ο_one, hasseDeriv_monomial, PowerSeries.trunc_trunc_pow, isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_neg_mul, Bivariate.pderiv_zero_equivMvPolynomial, cyclotomic_mul_prime_pow_eq, derivativeFinsupp_map, Splits.pow, mem_roots_iff_aeval_eq_zero, dickson_one_one_charP, degree_X_pow, IsLocalization.scaleRoots_commonDenom_mem_lifts, WeierstrassCurve.Affine.baseChange_polynomialX, monomial_add, one_lt_rootMultiplicity_iff_isRoot_gcd, WeierstrassCurve.preΞ¨'_odd, resultant_X_add_C_left, gal_X_sub_C_isSolvable, Bivariate.equivMvPolynomial_X, hasDerivWithinAt_aeval, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_eqβ, coeff_monomial_same, reesAlgebra.fg, evalβ_evalRingHom, Module.AEval.of_symm_X_smul, aeval_coe_eq_smeval, natDegree_pow_le_of_le, FiniteField.isSplittingField_of_card_eq, IsMonicOfDegree.aeval_add, natDegree_multiset_prod_X_sub_C_eq_card, C_dvd_iff_dvd_coeff, hasStrictDerivAt_aeval, dickson_one_one_zmod_p, MvPolynomial.natDegree_optionEquivLeft, span_of_finite_le_degreeLT, aeval_algebraMap_eq_zero_iff_of_injective, StandardEtalePresentation.exists_mul_aeval_x_g_pow_eq_aeval_x, Splits.C_mul_X_pow, bernsteinPolynomial.iterate_derivative_succ_at_0_eq_zero, iterate_derivative_eq_zero_of_degree_lt, toFinsuppIsoLinear_apply, exists_eq_X_add_C_of_natDegree_le_one, natSepDegree_smul_nonzero, Matrix.charpoly_coeff_eq_prod_coeff_of_le, PowerSeries.subst_coe, AdjoinRoot.Polynomial.quotQuotEquivComm_mk, RatFunc.denom_div, opRingEquiv_symm_C_mul_X_pow, WeierstrassCurve.Affine.CoordinateRing.exists_smul_basis_eq, MvPolynomial.mem_support_finSuccEquiv, isRoot_iterate_derivative_of_lt_rootMultiplicity, minpoly.aeval_algHom, mapAlgEquiv_toAlgHom, monic_expand_iff, iterate_derivative_prod_X_sub_C, monic_geom_sum_X, signVariations_eraseLead_mul_X_sub_C, eval_det, dvd_content_iff_C_dvd, natSepDegree_expand, coeff_C_succ, opRingEquiv_symm_monomial, toAddCircle_monomial_eq_smul_fourier, separable_C, instIsLocalHomRingHomC, aeval_apply_smul_mem_of_le_comap', X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd, cfc_eval_C, mahlerMeasure_X_sub_C, minpoly.add_algebraMap, MvPolynomial.rename_comp_toMvPolynomial, Ideal.isPrime_map_C_of_isPrime, PolynomialModule.equivPolynomialSelf_apply_eq, finiteMultiplicity_of_degree_pos_of_monic, MvPolynomial.finSuccEquiv_comp_C_eq_C, irreducible_of_degree_le_three_of_not_isRoot, degreeLT.addLinearEquiv_symm_apply, MulSemiringAction.charpoly_eq, Chebyshev.iterate_derivative_U_eval_one_recurrence, coe_basisMonomials, PowerSeries.trunc_apply, WeierstrassCurve.Affine.CoordinateRing.C_addPolynomial_slope, IsAdjoinRoot.adjoinRootAlgEquiv_apply_mk, WeierstrassCurve.Ο_odd, isMonicOfDegree_one_iff, root_X_pow_sub_C_pow, WeierstrassCurve.Ξ¨_even, bernsteinPolynomial.sum_mul_smul, LinearMap.aeval_self_charpoly, natDegree_X_pow_mul, WeierstrassCurve.Ξ¦_four, Mathlib.Tactic.ComputeDegree.natDegree_C_le, LaurentPolynomial.evalβ_toLaurent, coe_mapRingHom, C_mul_dvd, MvPolynomial.finSuccEquiv_eq, eval_mul_X_pow, isNilpotent_monomial_iff, as_sum_range', natDegree_monomial, mem_iff_annIdealGenerator_dvd, spectrum.subset_polynomial_aeval, PolyEquivTensor.toFunAlgHom_apply_tmul_eq_smul, factorial_mul_shiftedLegendre_eq, isNilpotent_iff, Chebyshev.one_sub_X_sq_mul_derivative_derivative_T_eq_poly_in_T, C_comp, natDegree_X_pow_le, IsAdjoinRootMonic.map_modByMonicHom, WeierstrassCurve.Affine.degree_polynomial, div_C, separable_def, aroots_quadratic_eq_pair_iff_of_ne_zero, comp_one, MvPolynomial.image_support_finSuccEquiv, iterate_derivative_smul, Ideal.mem_map_C_iff, natSepDegree_pow_of_ne_zero, isUnit_of_self_mul_dvd_separable, LieAlgebra.engel_isBot_of_isMin.lieCharpoly_coeff_natDegree, IsConjRoot.aeval_eq_zero, PowerSeries.IsWeierstrassDivisorAt.mod_smul, sumIDeriv_X, Bivariate.aevalAeval_swap, natDegree_pow_le, MulSemiringActionHom.coe_polynomial, coeff_X_pow_self, natDegree_pow, contentIdeal_monomial, dvd_C_mul_X_sub_one_pow_add_one, rootSet_C, injective_ofFn, matPolyEquiv_symm_C, toFinsupp_algebraMap, Bivariate.equivMvPolynomial_C_X, isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C, lifts_iff_coeff_lifts, PolyEquivTensor.toFunBilinear_apply_apply, natDegree_mul_C_eq_of_mul_ne_zero, coe_compRingHom, ofMultiset_apply, RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_apply, Module.AEval.mem_mapSubmodule_symm_apply, PolyEquivTensor.toFunLinear_tmul_apply, coeff_iterate_derivative, Cubic.prod_X_sub_C_eq, algHom_ext_iff, coeToPowerSeries.algHom_apply, Chebyshev.T_neg_two, rootMultiplicity_eq_multiplicity, bernoulli_def, Module.AEval.X_smul_of, derivative_evalβ_C, multiset_prod_X_sub_C_nextCoeff, C_div, Chebyshev.S_two, RatFunc.instIsScalarTowerOfPolynomial, Lagrange.nodal_eq_mul_nodal_erase, lhom_ext'_iff, Monic.irreducible_iff_degree_lt, PowerSeries.derivative_coe, natDegree_X_pow, divX_C_mul_X_pow, MvPolynomial.prod_X_add_C_coeff, MvPolynomial.degree_finSuccEquiv, Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, X_pow_mul_monomial, roots_expand_pow_map_iterateFrobenius, LaurentPolynomial.toLaurent_support, aeval_derivative_of_splits, evalEval_add, MvPolynomial.nonempty_support_optionEquivLeft, map_expand_pow_char, WeierstrassCurve.Ξ¨_zero, WeierstrassCurve.Ο_three, lsum_apply, Ideal.polynomialQuotientEquivQuotientPolynomial_symm_mk, WeierstrassCurve.Affine.baseChange_polynomial, coeff_expand_mul, cyclotomic_mul_prime_eq_pow_of_not_dvd, IsDistinguishedAt.algEquivQuotient_symm_apply, derivative_pow, isDomain_iff, C_ofNat, reverse_add_C, derivative_prod, IsPrimitiveRoot.squarefree_minpoly_mod, isSplittingField_C, not_irreducible_expand, AlgebraicClosure.Monics.map_eq_prod, LindemannWeierstrass.integral_exp_mul_eval, WeierstrassCurve.Ο_neg, isLocalization, expand_mul, eval_sumIDeriv_of_pos, aeval_continuousMap_apply, coe_aeval_mk_apply, dickson_one_one_eq_chebyshev_T, leadingCoeff_mul_C_of_isUnit, FiniteField.X_pow_card_sub_X_natDegree_eq, IsMonicOfDegree.pow, isRegular_X_pow, prod_cyclotomic_eq_geom_sum, coeff_zero_eq_aeval_zero, MvPolynomial.support_optionEquivLeft, not_isUnit_X_sub_C, FiniteField.splits_X_pow_card_sub_X, MvPolynomial.finSuccEquiv_X_succ, card_support_eq_two, Monic.geom_sum, cfc_polynomial, WeierstrassCurve.baseChange_Ο, polynomial_expand_eq, Chebyshev.iterate_derivative_U_eval_one, chebyshev_T_eq_dickson_one_one, span_minpoly_eq_annihilator, toFinsuppIsoAlg_symm_apply_toFinsupp, iterate_derivative_C_mul, reflect_C_mul_X_pow, card_support_eq_one, PolyEquivTensor.invFun_monomial, coe_expand, polynomialFunctions_coe, irreducible_factor, aroots_C_mul_X_pow, mkDerivation_one_eq_derivative, Matrix.charpoly_sub_diagonal_degree_lt, fourierCoeff_toAddCircle_natCast, leadingCoeff_C_mul_X, degreeLT.addLinearEquiv_symm_apply', spectrum.map_polynomial_aeval_of_degree_pos, constantCoeff_surjective, eraseLead_C, Splits.X_sub_C, isUnit_primPart_C, iterate_derivative_mul_X_pow, MvPolynomial.evalβ_const_pUnitAlgEquiv, evalβRingHom'_apply, IsAdjoinRootMonic.modByMonicHom_root_pow, annIdealGenerator_aeval_eq_zero, C_leadingCoeff_mul_prod_multiset_X_sub_C, coeff_inv_units, evalβ_pow, minpoly.eq_X_sub_C', smeval_pow, taylor_coeff_one, toContinuousMapAlgHom_apply, sup_ker_aeval_le_ker_aeval_mul, fderivWithin_aeval, PolyEquivTensor.toFunLinear_one_tmul_one, fderivWithin, monomial_neg, hasDerivAt, Monic.comp_X_add_C, divX_C, StandardEtalePresentation.toPresentation_Ο', monomial_zero_right, associated_of_dvd_of_natDegree_le_of_leadingCoeff, cyclotomic_eq_prod_X_pow_sub_one_pow_moebius, Monic.C_dvd_iff_isUnit, iterate_derivative_sub, coeff_X_add_one_pow, monic_mul_C_of_leadingCoeff_mul_eq_one, signVariations_monomial, natSepDegree_C, IsIntegrallyClosed.eq_map_mul_C_of_dvd, Derivation.map_aeval, matPolyEquiv_eval_eq_map, monic_mul_leadingCoeff_inv, eq_X_sub_C_of_splits_of_single_root, Splits.aeval_eq_prod_aroots_of_monic, card_support_C_mul_X_pow_le_one, PolyEquivTensor.left_inv, monomial_mul_X_pow, matPolyEquiv_coeff_apply, discr_C, aeval_neg, coeToPowerSeries.ringHom_apply, support_C_mul_X_pow, aeval_derivative_mem_differentIdeal, MvPolynomial.prod_C_add_X_eq_sum_esymm, modByMonic_X_sub_C_eq_C_eval, denomsClearable_C_mul_X_pow, binomial_eq_binomial, taylorEquiv_symm, iterate_derivative_X_pow_eq_C_mul, Matrix.charpoly_vecMulVec, derivative_X_pow, exists_monic_aeval_eq_zero_forall_mem_pow_of_mem_map, coeff_expand, MvPolynomial.finSuccEquiv_apply, sumIDeriv_derivative, rootsExpandToRoots_apply, degree_C_mul, X_dvd_iff, X_mul_monomial, gaussNorm_C, StandardEtalePair.HasMap.isUnit_derivative_f, Splits.eq_prod_roots_of_monic, AdjoinRoot.mk_X, leadingCoeff_expand, isNilpotent_C_mul_pow_X_of_isNilpotent, aeval_sumIDeriv_eq_eval, leadingCoeff_X_sub_C, Monic.pow, Matrix.isUnit_charpolyRev_of_isNilpotent, expand_eq_C, RatFunc.num_div_dvd', IsCoprime.wronskian_eq_zero_iff, WeierstrassCurve.Ξ¦_two, aeval_C, PowerBasis.exists_eq_aeval', evalEval_neg, aeval_eq_prod_aroots_sub_of_splits, KaehlerDifferential.polynomial_D_apply, toLaurent_inj, leval_apply, X_pow_mem_lifts, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk, MvPolynomial.rename_polynomial_aeval_X, ofFn_degree_lt, taylor_monomial, comp_eq_aeval, Lagrange.interpolate_apply, IsPurelyInseparable.minpoly_eq_X_pow_sub_C, C_mul, valuation_aeval_monomial_eq_valuation_pow, LinearMap.charpoly_one, natDegree_X_sub_C_le, splits_X_sub_C_mul_iff, factorial_smul_hasseDeriv, toMvPolynomial_X, FiniteField.minpoly_frobeniusAlgHom, dickson_of_two_le, Matrix.coeff_det_one_add_X_smul_one, aeval_ofReal, Chebyshev.one_sub_X_sq_mul_iterate_derivative_T_eq_poly_in_T, degree_add_degree_leadingCoeff_inv, toFinsupp_sum, evalβAddMonoidHom_apply, trinomial_def, hasDerivAt_aeval, coe_algebraMap_eq_CC, aeval_root_derivative_of_splits, X_sub_C_scaleRoots, Chebyshev.aeval_C, PerfectField.separable_iff_squarefree, iterate_derivative_neg, aeval_eq_sum_range, polyEquivTensor_apply, resultant_C_zero_left, C_eq_or_isOpenQuotientMap_eval, PolyEquivTensor.toFunBilinear_apply_eq_smul, MvPolynomial.eval_toMvPolynomial, X_pow_sub_X_sub_one_irreducible_rat, instFree, sum_taylor_eq, taylor_eval_sub, Chebyshev.aeval_U, derivative_prod_finset, mem_normalizedFactors_iff, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span, isNilpotent_C_iff, disc_C, X_mem_nonzeroDivisors, Differential.deriv_aeval_eq, MvPolynomial.irreducible_toPolynomialAdjoinImageCompl, hasseDeriv_C, Algebra.exists_aeval_invOf_eq_zero_of_idealMap_adjoin_sup_span_eq_top, natDegree_linear_le, MvPolynomial.toMvPowerSeries_pUnitAlgEquiv, MvPolynomial.transcendental_polynomial_aeval_X, coeff_list_sum, Ideal.factors_span_eq, derivation_C, minpoly_algEquiv_toLinearMap, smeval_monomial, natDegree_det_X_add_C_le, eval_C_X_comp_evalβ_map_C_X, AdjoinRoot.algHom_subsingleton, toLaurent_one, homogenize_monomial_of_lt, mod_X_sub_C_eq_C_eval, StandardEtalePair.cond, Chebyshev.one_sub_X_sq_mul_U_eq_pol_in_T, StandardEtalePresentation.aeval_val_equivMvPolynomial, PolynomialModule.eval_smul, smul_C, derivative_sub, mem_rootSet', AdjoinRoot.Polynomial.quotQuotEquivComm_symm_mk_mk, geom_sum_X_comp_X_add_one_eq_sum, hasStrictDerivAt, LinearMap.charpoly_sub_smul, Bivariate.swap_C, minpoly.neg, cyclotomic.irreducible_rat, natSepDegree_X_sub_C, coe_normUnit, RatFunc.algebraMap_apply, instFaithfulSMulPolynomial, aroots_monomial, det_taylorLinearEquiv, WeierstrassCurve.Affine.CoordinateRing.coe_norm_smul_basis, PowerSeries.trunc_one, aroots_X_pow, degree_sum_eq_of_disjoint, derivative_monomial_succ, NormedAlgebra.Real.exists_isMonicOfDegree_two_and_aeval_eq_zero, resultant_deriv, degree_le_zero_iff, IsAdjoinRoot.algebraMap_apply, support_X_pow, spectralValue_X_sub_C, StandardEtalePair.aeval_X_g_mul_mk_X, Transcendental.aeval, PowerSeries.trunc_succ, roots_C_mul_X_sub_C, MvPolynomial.evalβ_pUnitAlgEquiv_symm, monomial_one_right_eq_X_pow, Derivation.compAEval_eq, hasseDeriv_apply_one, aeval_endomorphism, WeierstrassCurve.Affine.CoordinateRing.mk_Οβ_sq, IntermediateField.mem_adjoin_simple_iff, rootMultiplicity_le_iff, eraseLead_mul_eq_mul_eraseLead_of_nextCoeff_zero, isUnit_iff_degree_eq_zero, surjective_toFn, modByMonic_X, IsPurelyInseparable.minpoly_eq_X_sub_C_pow, WeierstrassCurve.Affine.CoordinateRing.basis_zero, Module.AEval.of_aeval_smul, map_sum, Algebra.mem_ideal_map_adjoin, X_pow_sub_C_irreducible_of_prime_pow, minpoly.not_isUnit, mem_aroots, integralNormalization_mul_C_leadingCoeff, eval_sum, bernsteinPolynomial.derivative_succ, ZMod.expand_card, roots_quadratic_eq_pair_iff_of_ne_zero', PowerSeries.IsWeierstrassDivision.isWeierstrassFactorization, lifts_iff_liftsRing, iterate_derivative_X_sub_pow_self, derivativeFinsupp_one, X_dvd_sub_C, IsAdjoinRoot.map_self, degreeLT_eq_span_X_pow, eval_mul_X_sub_C, MvPolynomial.polynomial_eval_evalβ, WeierstrassCurve.Affine.map_polynomialX, minpolyDiv_spec, isNilpotent_mul_X_iff, reverse_C, Splits.C_mul, cardPowDegree_nonzero, toFinsuppIsoAlg_apply, reflect_C, evalβ_C, taylor_zero, Ideal.jacobson_bot_polynomial_of_jacobson_bot, comp_zero, toMatrix_sylvesterMap, PowerSeries.coeff_mul_eq_coeff_trunc_mul_trunc, MvPolynomial.optionEquivLeft_monomial, RatFunc.ofFractionRing_eq, reflect_C_mul, derivative_neg, aeval_algEquiv, Matrix.charpoly_inv, deriv, evalβ_pow', support_subset_support_matPolyEquiv, algEquivAevalNegX_apply, natDegree_sub_C, Module.End.ker_aeval_ring_hom'_unit_polynomial, PowerSeries.trunc_coe_eq_self, PrimeSpectrum.range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, MvPolynomial.optionEquivLeft_symm_apply, Algebra.FinitePresentation.polynomial, hasseDeriv_natDegree_eq_C, hasFDerivWithinAt_aeval, as_sum_range_C_mul_X_pow, Submodule.IsPrincipal.contentIdeal_generator_dvd, contDiff_aeval, IsAdjoinRoot.ofAlgEquiv_map_apply, isNilpotent_reflect_iff, matPolyEquiv_symm_map_eval, AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_mk, mem_reesAlgebra_iff, derivative_C_mul_X_pow, signVariations_X_sub_C_mul_eraseLead_le, support_binomial, MvPolynomial.mem_support_coeff_finSuccEquiv, derivative_C, FunctionField.ringOfIntegers.instIsNoetherianPolynomialSubtypeMemSubalgebraOfIsSeparableRatFunc, roots_X_pow_char_sub_C, degree_mul_C_of_isUnit, mem_rootSet, AdjoinRoot.minpoly_powerBasis_gen, AdjoinRoot.aeval_algHom_eq_zero, derivative_bernoulli_add_one, hasseDeriv_apply, addSubmonoid_closure_setOf_eq_monomial, map_under_lt_comap_of_quasiFiniteAt, dickson_two_one_eq_chebyshev_U, evalβ_derivative_of_splits, natTrailingDegree_X_pow, Separable.squarefree, C_mul_comp, IsAdjoinRoot.map_eq_zero_iff, Algebra.FiniteType.instPolynomial, Module.End.IsSemisimple.minpoly_squarefree, roots_expand_image_iterateFrobenius, sum_modByMonic_coeff, Chebyshev.iterate_derivative_U_eval_one_eq_div, aeval_monomial, eval_map_algebraMap, Algebra.Norm.Transitivity.eval_zero_det_det, mapAlgEquiv_coe_ringHom, AdjoinRoot.quotEquivQuotMap_symm_apply, bernoulli_one, Chebyshev.iterate_derivative_T_eval_one, NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply, StandardEtalePresentation.toPresentation_val, algEquivOfCompEqX_apply, Ideal.isDomain_map_C_quotient, matPolyEquiv_eval, isIntegrallyClosed_iff', mem_rootSet_of_ne, mapAlg_comp, sylvesterMap_apply_coe, IsAdjoinRoot.aeval_root_self, natDegree_mul_C_le, aeval_eq_sum_range', degreeLT.addLinearEquiv_natAdd, expand_char, aeval_zero, leadingCoeff_X_pow_sub_one, Chebyshev.C_eq_two_mul_T_comp_half_mul_X, MvPolynomial.pUnitAlgEquiv_monomial, conductor_mul_differentIdeal, support_derivativeFinsupp_subset_range, mapRingHom_id, ofFn_comp_toFn_eq_id_of_natDegree_lt, monomial_zero_left, natDegree_mul_C, Module.AEval.annihilator_top_eq_ker_aeval, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk, FiniteField.X_pow_card_pow_sub_X_natDegree_eq, WeierstrassCurve.Ο_four, roots_expand_pow_image_iterateFrobenius_subset, rootMultiplicity_X_sub_C_self, taylor_coeff, minpoly.eq_iff_aeval_minpoly_eq_zero, splits_X_sub_C, algEquivCMulXAddC_symm_apply, taylor_inj, Chebyshev.T_eq_half_mul_C_comp_two_mul_X, derivative_zero, opRingEquiv_symm_C, evalEval_zero, IsAlgClosed.roots_eq_zero_iff, exists_irreducible_of_natDegree_ne_zero, natDegree_cubic, degree_leadingCoeff_inv, irreducible_X, IsMonicOfDegree.aeval_sub, MvPolynomial.finSuccEquiv_rename_finSuccEquiv, not_isUnit_X_pow_sub_one, ContinuousMap.polynomial_comp_attachBound, toFinsupp_C_mul_X_pow, expand_eval, logMahlerMeasure_const, natDegree_C_mul_of_isUnit, hermite_zero, Monic.not_irreducible_iff_exists_add_mul_eq_coeff, Monic.irreducible_iff_natDegree', isAlgebraic_iff_not_injective, dickson_two, succ_signVariations_X_sub_C_mul_monomial, derivative_X_add_C_sq, one_lt_rootMultiplicity_iff_isRoot_iterate_derivative, span_le_degreeLE_of_finite, cyclotomic_three, as_sum_support, FiniteField.expand_card, taylorLinearEquiv_symm, coeff_expand_mul', comp_eq_sum_left, differentiableWithinAt_aeval, rootMultiplicity_X_sub_C, AdjoinRoot.coe_algEquivOfEq, natTrailingDegree_monomial_le, AdjoinRoot.aeval_eq, Matrix.charpoly_mul_comm', evalβ_multiset_sum, coeff_zero_eq_aeval_zero', PowerSeries.evalβ_trunc_eq_sum_range, IsLocalization.adjoin_inv, degreeLT.addLinearEquiv_symm_apply_inl_basis, PowerSeries.trunc_one_X, leval_coe_eq_smeval, map_dvd_map, dvd_comp_X_sub_C_iff, LaurentPolynomial.leftInverse_trunc_toLaurent, roots_expand_pow, AnalyticOnNhd.aeval_polynomial, evalEval_map_C, pow_mul_divByMonic_rootMultiplicity_eq, contract_mul_expand, algEquivAevalXAddC_apply, leadingCoeff_C, PolynomialModule.monomial_smul_apply, map_frobenius_expand, natDegree_coe_units, Module.AEval.instFinitePolynomial, logMahlerMeasure_monomial, cauchyBound_X_add_C, degree_cubic_le, PowerSeries.trunc_trunc, WeierstrassCurve.Ξ¨_four, leadingCoeff_X_pow_add_one, rootSet_monomial, matPolyEquiv_symm_X, monomial_left_inj, evalEval_list_prod, aeval_pi, newtonMap_apply, Derivation.apply_aeval_eq', toLaurent_C_mul_eq, X_sub_C_mul_removeFactor, aevalTower_comp_C, logMahlerMeasure_C_mul_X_add_C, not_isUnit_X, Cubic.eq_prod_three_roots, FiniteField.isSplittingField_sub, coe_aeval_eq_eval, Matrix.aeval_self_charpoly, leadingCoeff_pow, exists_irreducible_of_natDegree_pos, Multiset.prod_X_add_C_eq_sum_esymm, coeff_C_zero, natDegree_iterate_derivative, Monic.nextCoeff_pow, exists_prod_multiset_X_sub_C_mul, degree_linear_le, smul_modByMonic, IsAdjoinRoot.algEquiv_map, mapAlgHom_comp, Matrix.charmatrix_apply, instFiniteTypeSubtypePolynomialMemSubalgebraReesAlgebraOfIsNoetherianRing, eval_add_of_sq_eq_zero, scaleRoots_zero, derivative_X_add_C_pow, homogenize_C, PowerSeries.aeval_coe, cyclotomic_prime, content_C, eval_multisetSum, splits_iff_exists_multiset', toFinsupp_C_mul_X, natDegree_monomial_eq, minpoly.natSepDegree_eq_one_iff_eq_expand_X_sub_C, Monic.expand, dvd_iff_isRoot, iterate_derivative_mul, mapRingHom_comp, Chebyshev.T_eq_X_mul_T_sub_pol_U, qsmul_eq_C_mul, derivative_map, Multiset.prod_X_add_C_coeff', splits_X_pow, PowerSeries.substAlgHom_coe, degree_linear_lt_degree_C_mul_X_sq, LinearMap.charpoly_zero, cauchyBound_X_sub_C, splits_of_exists_multiset, map_C, rootSet_X_pow, iterate_derivative_intCast_mul, taylor_mem_degreeLT, C_neg, leadingCoeff_monomial, Lagrange.eval_nodal_derivative_eval_node_eq, MvPolynomial.rename_toMvPolynomial, natDegree_expand, Module.Basis.traceDual_powerBasis_eq, isNilpotent_pow_X_mul_C_of_isNilpotent, prod_X_sub_C_coeff_card_pred, evalEval_smul, card_support_le_one_iff_monomial, MvPolynomial.optionEquivLeft_symm_C_X, not_irreducible_C, coeff_mul_monomial, degree_quadratic_lt_degree_C_mul_X_cb, coeff_C_mul_X_pow, LaurentPolynomial.trunc_C_mul_T, aeval_pi_applyβ, derivative_natCast, WeierstrassCurve.Ο_two, degree_C_mul_X, MvPolynomial.finSuccEquiv_X_zero, comp_X_add_C_eq_zero_iff, MvPolynomial.degreeOf_eq_natDegree, resultant_X_sub_C_left, hasseDeriv_X, lifts_iff_set_range, aeval_mem_adjoin_singleton, spectralValue_eq_zero_iff, toLaurent_X, derivative_bernoulli, scaleRoots_C, evalβAlgHom'_apply, LieAlgebra.engel_isBot_of_isMin.lieCharpoly_natDegree, toAddCircle_X_eq_fourier_one, AdjoinRoot.mk_self, WeierstrassCurve.Ξ¨Sq_three, ofFn_coeff_eq_val_of_lt, coeff_mul_X_pow', evalEval_surjective, degree_pow', PolynomialModule.monomial_smul_lsingle, tendsto_abv_aeval_atTop, Lagrange.nodal_subgroup_eq_X_pow_card_sub_one, degree_mul_C, LinearMap.not_hasEigenvalue_zero_tfae, MvPolynomial.transcendental_supported_polynomial_aeval_X_iff, div_C_mul, resultant_C_mul_left, resultant_pow_left, StandardEtalePresentation.toPresentation_relation, cyclotomic_expand_eq_cyclotomic, map_mapRingHom_eval_map, toMvPolynomial_injective, roots_X_pow, opRingEquiv_op_C_mul_X_pow, degreeLT.basisProd_natAdd, Ideal.polynomialQuotientEquivQuotientPolynomial_map_mk, PowerSeries.WithPiTopology.tendsto_trunc_atTop, roots_X_add_C, WeierstrassCurve.Affine.baseChange_polynomialY, monomial_natDegree_leadingCoeff_eq_self, degreeLE_mono, aeval_algHom_apply, coe_toLaurentAlg, WeierstrassCurve.Ξ¨Sq_four, PowerSeries.IsWeierstrassDivisionAt.smul, hilbertPoly_mul_one_sub_pow_add, Ideal.quotient_mk_maps_eq, RatFunc.toFractionRingRingEquiv_symm_eq, shiftedLegendre_eval_symm, bernsteinPolynomial.derivative_zero, iterate_derivative_map, sumIDeriv_apply_of_le, RatFunc.aeval_X_left_eq_algebraMap, Bivariate.pderiv_one_equivMvPolynomial, support_monomial', WeierstrassCurve.map_Ο, mem_degreeLE, isScalarTower_right, X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd, separable_C_mul_X_pow_add_C_mul_X_add_C, Monic.irreducible_iff_irreducible_map_fraction_map, Matrix.IsHermitian.charpoly_eq, RatFunc.associated_num_inv, bernsteinPolynomial.iterate_derivative_at_0_eq_zero_of_lt, taylor_X, multiset_prod_X_sub_C_coeff_card_pred, separable_X_sub_C, mapAlgHom_coe_ringHom, bernsteinPolynomial.iterate_derivative_at_0, finiteMultiplicity_X_sub_C, Chebyshev.derivative_U_eval_one_eq_div, WeierstrassCurve.Affine.CoordinateRing.XYIdeal'_eq, hasFDerivWithinAt, Algebra.IsInvariant.charpoly_mem_lifts, MvPolynomial.optionEquivLeft_elim_eval, MvPolynomial.optionEquivLeft_symm_X, leadingCoeff_X_add_C, degree_sum_fin_lt, minpoly.irreducible, IsEisensteinAt.irreducible, expand_aeval, ringHom_ext'_iff, irreducible_X_sub_C, not_dvd_of_natDegree_lt, Monic.as_sum, ofFinsupp_sum, degreeLE_eq_span_X_pow, matPolyEquiv_coeff_apply_aux_2, aeval_natCast, aevalTower_comp_toAlgHom, iterate_derivative_one, preimage_eval_singleton, mem_nonzeroDivisors_of_coeff_mem, IsPrimitive.isUnit_iff_isUnit_map, natDegree_derivative_lt, MvPolynomial.aeval_comp_toMvPolynomial, Cubic.C_mul_prod_X_sub_C_eq, aeval_algHom, coe_aevalAeval_eq_evalEval, map_mapRingHom_eval_map_eval, toLaurent_C, eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le, ofMultiset_injective, IsSplittingField.IsScalarTower.splits, PowerBasis.aeval_minpolyGen, X_pow_comp, Chebyshev.one_sub_X_sq_mul_iterate_derivative_U_eq_poly_in_U, coe_aeval_eq_evalRingHom, RatFunc.algebraMap_monomial, instFiniteDimensionalQuotientPolynomialIdealSpanSingletonSetSmithCoeffs, AdjoinRoot.coe_algHomOfDvd, bernoulli_comp_one_sub_X, toLaurentAlg_apply, taylor_pow, evalEval_natCast, irreducible_C_mul_X_add_C, smul_X_eq_monomial, commute_X_pow, Chebyshev.C_two, resultant_X_pow_left, succ_signVariations_le_X_sub_C_mul, one_lt_rootMultiplicity_iff_isRoot, monomial_sub, coeff_monomial_succ, Splits.C, MvPolynomial.evalβ_pUnitAlgEquiv, PowerSeries.trunc_sub, annIdealGenerator_eq_zero_iff, le_trailingDegree_X_pow, reverse_C_add, natDegree_linear, matPolyEquiv_smul_one, autAdjoinRootXPowSubC_root, degree_monomial, spectrum.map_polynomial_aeval, toLaurent_C_mul_X_pow, Ideal.isPrime_map_C_iff_isPrime, pow_scaleRoots', PowerSeries.trunc_derivativeFun, Matrix.charpoly_diagonal, degree_mul_X_pow, degree_add_C, sylveserMap_comp_adjSylvester, toAddCircle_C_eq_smul_fourier_zero, evalEval_C, algHom_ext'_iff, isLocalHom_expand, coe_evalβRingHom, natDegree_pow_X_add_C, LaurentPolynomial.toLaurent_reverse, PowerSeries.trunc_map, natDegree_eq_zero, ker_modByMonicHom, Monic.irreducible_of_degree_eq_one, Mathlib.Tactic.ComputeDegree.coeff_pow_of_natDegree_le_of_eq_ite', map_evalRingHom_eval, isNilpotent_reverse_iff, PowerSeries.coeff_coe_trunc_of_lt, IsUnitTrinomial.irreducible_aux1, roots_C_mul_X_add_C_of_IsUnit, isMonicOfDegree_monomial_one, PowerSeries.trunc_zero', mirror_C, bernoulli_comp_neg_X, MvPolynomial.optionEquivLeft_symm_C_C, Derivation.compAEval_apply, Cubic.of_c_eq_zero, matPolyEquiv_eq_X_pow_sub_C, cyclotomic_eq_X_pow_sub_one_div, hasseDeriv_eq_zero_of_lt_natDegree, spectralValue_X_pow, coeff_divByMonic_X_sub_C, ofFn_coeff_eq_zero_of_ge, degreeLT.basisProd_castAdd, Matrix.derivative_det_one_add_X_smul_aux, degree_C_mul_X_pow, trailingDegree_monomial, C_pow, C_add, coe_taylorEquiv, hasDerivWithinAt, zero_notMem_multiset_map_X_add_C, Matrix.charpoly_ofNat, Matrix.aeval_eq_aeval_mod_charpoly, mod_def, aeval_algebraMap_apply, PowerSeries.trunc_derivative, AdjoinRoot.algEquivOfEq_toAlgHom, leadingCoeff_divByMonic_X_sub_C, bernsteinPolynomial.derivative_succ_aux, pairwise_coprime_X_sub_C, WeierstrassCurve.Ο_zero, derivative_X_sub_C, MvPolynomial.IsHomogeneous.finSuccEquiv_coeff_isHomogeneous, fourierCoeff_toAddCircle, IsDistinguishedAt.algEquivQuotient_apply, natSepDegree_X_pow, Module.AEval.mem_mapSubmodule_apply, aroots_C, isMonicOfDegree_X_pow, minpoly.ker_eval, minpoly.eq_X_sub_C, cyclotomic_prime_mul_X_sub_one, roots_C, Chebyshev.C_neg_two, mapAlgHom_id, Matrix.charmatrix_diagonal, Lagrange.nodal_erase_eq_nodal_div, monic_prod_X_sub_C, LaurentPolynomial.instIsScalarTowerPolynomial, natDegree_cubic_le, ConjRootClass.irreducible_minpoly, card_roots_toFinset_le_derivative, map_aeval_eq_aeval_map, adjoin_X, IsAlgClosed.associated_iff_roots_eq_roots, iterate_derivative_sum, Chebyshev.one_sub_X_sq_mul_iterate_derivative_T_eval, WeierstrassCurve.Ο_four, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of, Module.AEval.annihilator_eq_ker_aeval, Bivariate.equivMvPolynomial_C_C, WeierstrassCurve.Ξ¨_odd, natDegree_quadratic, RatFunc.laurentAux_ofFractionRing_mk, natDegree_C_mul_X_pow_le, aeval_add, instIsLocalHomRingHomAlgebraMap, continuousOn_aeval, aeval_sub, coe_pow, IsAdjoinRoot.map_surjective, sumIDeriv_apply_of_lt, mem_lift_of_splits_of_roots_mem_range, erase_monomial, continuousAt_aeval, IsSepClosed.exists_aeval_eq_zero, card_roots_sub_C, integralClosure.mem_lifts_of_monic_of_dvd_map, homogenizeLM_apply, degree_derivative_le, Module.End.eigenspace_aeval_polynomial_degree_1, inv_eq_of_aeval_divX_ne_zero, Chebyshev.iterate_derivative_T_eval_one_eq_div, lifts_iff_coeffs_subset_range, isRoot_of_isRoot_iff_dvd_derivative_mul, exists_monic_aeval_eq_zero_forall_mem_of_mem_map, resultant_C_mul_right, derivative_one, taylorLinearEquiv_apply_coe, PowerSeries.natDegree_trunc_lt, irreducible_of_degree_eq_one, coe_evalEvalRingHom, degree_linear, Chebyshev.derivative_T_eval_one, WeierstrassCurve.Affine.CoordinateRing.basis_apply, taylor_C, LindemannWeierstrass.hasDerivAt_cexp_mul_sumIDeriv, Transcendental.aeval_of_transcendental, mem_degreeLT, derivative_apply, PowerSeries.trunc_X, mem_map_rangeS, C_injective, aeval_X, degreeLT.basis_repr, LaurentPolynomial.exists_T_pow, polyEquivTensor_symm_apply_tmul_eq_smul, nextCoeff_C_mul, AdjoinRoot.mkβ_toRingHom, self_sub_C_mul_X_pow, monomial_comp, natDegree_add_C, IsAdjoinRoot.algEquiv_apply_map, coe_evalRingHom, eval_C_mul, roots_expand_map_frobenius_le, isCoprime_X_sub_C_of_isUnit_sub, irreducible_X_pow_sub_C_of_root_adjoin_eq_top, evalβ_evalβRingHom_apply, ofFn_natDegree_lt, isNoetherianRing, aeval_homogenize_of_eq_one, toContinuousMapOnAlgHom_apply, evalEval_one, neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq, IsAdjoinRoot.ker_map, monomial_mul_monomial, coe_mapAlgHom, content_X_pow, RatFunc.associated_denom_inv, signVariations_C_mul, MvPolynomial.totalDegree_coeff_optionEquivLeft_le, Monic.irreducible_iff_roots_eq_zero_of_degree_le_three, trailingDegree_X_pow, mkDerivation_apply, not_finite, coeff_monomial_mul, Module.instFinitePolynomialAEval', Lagrange.interpolate_singleton, C_content_dvd, galois_poly_separable, Ideal.Filtration.submodule_fg_iff_stable, coeff_X_add_C_pow, WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_Y, degree_linear_lt, WeierstrassCurve.preΞ¨_even, PowerSeries.trunc_C_mul, Chebyshev.add_one_mul_T_eq_poly_in_U, coeffList_monomial, algEquivAevalXAddC_symm, evalEval_mul, degree_coe_units, IsAlgClosed.exists_aeval_eq_zero, expand_injective, natDegree_pow', coeff_det_X_add_C_zero, derivative_C_mul_X_sq, content_monomial, Lagrange.nodal_eq, derivativeFinsupp_C, card_support_trinomial, LieAlgebra.engel_isBot_of_isMin.lieCharpoly_monic, taylor_one, X_pow_sub_C_irreducible_iff_of_prime, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_mul_XYIdeal, irreducible_of_dvd_cyclotomic_of_natDegree, AdjoinRoot.mk_C, map_iterateFrobenius_expand, derivativeFinsupp_X, roots_X_pow_char_pow_sub_C, RatFunc.eval_algebraMap, exists_irreducible_of_degree_pos, evalβ_algebraMap_X, LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul, toMvPolynomial_C, exists_mul_add_mul_eq_C_resultant, Matrix.charpoly_of_card_eq_two, eval_multiset_prod_X_sub_C_derivative, toFinsupp_C, smeval_mul_X_pow, X_sub_C_pow_dvd_iff, lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors', aroots_pow, Matrix.charmatrix_zero, natDegree_multiset_sum_le, isCyclic_tfae, roots_prod_X_sub_C, add_scaleRoots_of_natDegree_eq, bernsteinPolynomial.iterate_derivative_at_1, cfc_comp_polynomial, Lagrange.nodalWeight_eq_eval_derivative_nodal, derivative_intCast, C_smul_derivation_apply, leadingCoeff_taylor, homogenize_monomial, X_pow_mul_C, AdjoinRoot.evalEval_mk, derivative_add, expand_pow, degree_sub_C, map_taylorEquiv_degreeLT, PowerBasis.liftEquiv_apply_coe, Multiset.prod_X_sub_C_coeff, IsPrimitiveRoot.minpoly_dvd_x_pow_sub_one, degree_X_add_C, eval_geom_sum, monomial_add_erase, isMonicOfDegree_sub_add_two, algebraMap_eq, coe_mapAlgEquiv, cyclotomic'_eq_X_pow_sub_one_div, X_pow_mul, degree_C_le, eval_monomial, Monic.neg_one_pow_natDegree_mul_comp_neg_X, IsAdjoinRootMonic.modByMonic_repr_map, fourierCoeff_toAddCircle_eq_zero_of_lt_zero, MvPolynomial.transcendental_supported_polynomial_aeval_X, GaloisField.splits_zmod_X_pow_sub_X, aeval_sumIDeriv_of_pos, MvPolynomial.eval_polynomial_eval_finSuccEquiv, monic_X_pow_sub, continuousWithinAt_aeval, Monic.eq_X_sub_C_pow_of_natSepDegree_eq_one_of_splits, KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span, Derivation.apply_aeval_eq, PowerSeries.trunc_derivative', KummerDedekind.quotMapEquivQuotQuotMap_symm_apply, RatFunc.toFractionRing_eq, Matrix.isNilpotent_charpoly_sub_pow_of_isNilpotent
|
smulZeroClass π | CompOp | 58 mathmath: degree_smul_of_smul_regular, Mathlib.Tactic.ComputeDegree.degree_smul_le_of_le, nnqsmul_eq_C_mul, homogenize_smul, sum_smul_index', derivative_smul, natDegree_smul, C_mul', monic_of_isUnit_leadingCoeff_inv_smul, AdjoinRoot.smul_mk, natDegree_smul_of_smul_regular, smul_monomial, sum_smul_index, smul_eq_C_mul, isScalarTower, cauchyBound_smul, smeval_smul, prodXSubSMul.smul, IsSMulRegular.polynomial, MulSemiringAction.charpoly_eq_prod_smul, MulSemiringAction.smul_charpoly, Mathlib.Tactic.ComputeDegree.natDegree_smul_le_of_le, smul_X, coe_smul, smul_eq_map, smul_eval_smul, isCentralScalar, iterate_derivative_X_pow_eq_smul, ofFinsupp_smul, leadingCoeff_smul_of_smul_regular, degree_smul_of_isRightRegular_leadingCoeff, coeff_smul, support_smul, PolyEquivTensor.toFunAlgHom_apply_tmul_eq_smul, iterate_derivative_smul, FixedPoints.smul_polynomial, PolyEquivTensor.toFunBilinear_apply_apply, natDegree_smul_le, map_smul, degree_smul_le, PolyEquivTensor.toFunBilinear_apply_eq_smul, smul_C, toFinsupp_smul, eval_smul, faithfulSMul, scaleRoots_zero, smul_eval, smulCommClass, qsmul_eq_C_mul, evalEval_smul, mirror_smul, evalβ_smul, isScalarTower_right, smul_X_eq_monomial, eval_smul', smul_comp, polyEquivTensor_symm_apply_tmul_eq_smul, Mathlib.Tactic.ComputeDegree.coeff_smul
|
sum π | CompOp | 40 mathmath: PolyEquivTensor.toFunBilinear_apply_eq_sum, expand_eq_sum, sum_smul_index', PolyEquivTensor.toFunAlgHom_apply_tmul, derivative_eval, sum_C_index, sum_smul_index, sum_X_index, evalEval_sum, sum_add, evalβ_sum, sum_C_mul_X_pow_eq, polyEquivTensor_symm_apply_tmul, sum_monomial_index, sum_monomial_eq, smul_sum, mul_eq_sum_sum, sum_eq_of_subset, evalβ_def, coeff_sum, sum_add_index, lsum_apply, smeval_def, sum_def, eval_eq_sum, sum_over_range, sum_taylor_eq, sum_fin, sum_zero_index, aeval_endomorphism, eval_sum, sum_over_range', hasseDeriv_apply, smeval_eq_sum, comp_eq_sum_left, coeff_mul_mirror, evalβ_eq_sum, mahlerMeasure_le_sum_norm_coeff, derivative_apply, sum_add'
|
support π | CompOp | 89 mathmath: supp_subset_range, support_monomial, MvPolynomial.support_finSuccEquiv, support_trinomial, support_C_mul_X, card_support_le_one_of_eraseLead_eq_zero, eraseLead_support, iterate_derivative_eq_factorial_smul_sum, card_support_eraseLead_add_one, natDegree_notMem_eraseLead_support, support_C_mul_X', MvPolynomial.nonempty_support_finSuccEquiv, IsLocalization.coeffIntegerNormalization_mem_support, mem_support_derivative, MvPolynomial.support_finSuccEquiv_nonempty, support_trinomial', isUnitTrinomial_iff, support_neg, support_scaleRoots_eq, support_binomial', support_C, hilbertPoly_succ, as_sum_support_C_mul_X_pow, card_support_eq, mem_support_iff, natDegree_eq_support_max', support_ofFinsupp, IsUnitTrinomial.card_support_eq_three, card_support_binomial, support_C_subset, support_C_mul_X_pow', support_X, card_support_eq', support_update_zero, card_support_mul_le, supp_subset_range_natDegree_succ, mul_eq_sum_sum, support_add, reflect_support, card_support_eq_three, card_supp_le_succ_natDegree, iterate_derivative_eq_sum, notMem_support_iff, supNorm_def', support_integralNormalization_subset, IsLocalization.scaleRoots_commonDenom_mem_lifts, MvPolynomial.mem_support_finSuccEquiv, support_smul, support_toSubring, sum_sq_norm_coeff_eq_circleAverage, support_opRingEquiv, natTrailingDegree_eq_support_min', card_support_eraseLead, card_support_eq_zero, support_integralNormalization, LaurentPolynomial.toLaurent_support, MvPolynomial.nonempty_support_optionEquivLeft, MvPolynomial.support_optionEquivLeft, card_support_eq_two, card_support_eq_one, support_update, card_support_C_mul_X_pow_le_one, support_C_mul_X_pow, sum_def, natTrailingDegree_mem_support_of_nonzero, support_map_subset, eraseLead_support_card_lt, support_X_pow, nonempty_support_iff, support_update_ne_zero, support_subset_support_matPolyEquiv, support_binomial, support_eq_empty, natDegree_mem_support_of_nonzero, support_toFinsupp, as_sum_support, trinomial_support, mem_coeffs_iff, support_restriction, card_support_le_one_iff_monomial, card_support_eq_one_of_eraseLead_eq_zero, support_scaleRoots_le, support_monomial', support_erase, support_map_of_injective, support_zero, support_nonempty, support_X_empty, card_support_trinomial
|
toFinsupp π | CompOp | 38 mathmath: toFinsupp_zsmul, toFinsupp_pow, toFinsupp_monomial, toFinsupp_inj, toFinsupp_injective, toFinsupp_eq_zero, toFinsupp_nsmul, eta, toFinsupp_X_pow, toLaurent_apply, toFinsuppIsoLinear_symm_apply_toFinsupp, toFinsupp_one, toFinsupp_natCast, toFinsupp_ofNat, toFinsupp_mul, toFinsuppIsoLinear_apply, toFinsupp_algebraMap, toFinsupp_X, toFinsupp_eq_one, supDegree_eq_degree, toFinsuppIsoAlg_symm_apply_toFinsupp, toFinsuppIso_apply, toFinsupp_apply, toFinsupp_sum, toFinsupp_add, toFinsupp_neg, toFinsupp_smul, toFinsuppIsoAlg_apply, toFinsupp_sub, support_toFinsupp, toFinsupp_C_mul_X_pow, toFinsupp_C_mul_X, toFinsupp_intCast, supDegree_eq_natDegree, IsUnitTrinomial.irreducible_aux1, toFinsupp_erase, toFinsupp_zero, toFinsupp_C
|
toFinsuppIso π | CompOp | 2 mathmath: toFinsuppIso_apply, toFinsuppIso_symm_apply
|
toFinsuppIsoLinear π | CompOp | 2 mathmath: toFinsuppIsoLinear_symm_apply_toFinsupp, toFinsuppIsoLinear_apply
|
unique π | CompOp | β |
update π | CompOp | 10 mathmath: coeff_update_ne, update_zero_eq_erase, update_eq_add_sub_coeff, coeff_update_apply, support_update_zero, coeff_update_same, support_update, support_update_ne_zero, coeff_update, degree_update_le
|
Β«term_[X]Β» π | CompOp | β |