derivative 📖 | CompOp | 246 mathmath: fderiv, Lagrange.eval_iterate_derivative_eq_sum, Derivation.apply_eval_eq, derivative_X_sq, coeff_derivative, derivWithin_aeval, derivative_intCast_mul, eval_minpolyDiv_self, expNegInvGlue.hasDerivAt_polynomial_eval_inv_mul, derivative_C_mul, eval₂_minpolyDiv_self, iterate_derivative_zero, card_rootSet_le_derivative, derivative_mul, Chebyshev.one_sub_X_sq_mul_derivative_derivative_U_eq_poly_in_U, Lagrange.derivative_nodal, hensels_lemma, rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero, eval₂_minpolyDiv_of_eval₂_eq_zero, hasseDeriv_one', derivative_comp_one_sub_X, derivative_pow_eq_zero, aeval_iterate_derivative_of_ge, derivative_expand, derivative_sum, isCoveringMapOn_eval, derivative_pow_succ, sum_smul_minpolyDiv_eq_X_pow, derivative_ofNat, Splits.eval_derivative, derivative_smul, iterate_derivative_eq_factorial_smul_sum, iterate_derivative_X_add_pow, eval_minpolyDiv_of_aeval_eq_zero, derivative_X, dvd_iterate_derivative_pow, KaehlerDifferential.polynomialEquiv_D, abc, Splits.eval_root_derivative, derivative_monomial, Chebyshev.T_derivative_eq_U, aeval_iterate_derivative_self, Chebyshev.iterate_derivative_T_eval_one_recurrence, rootMultiplicity_sub_one_le_derivative_rootMultiplicity, Bivariate.Polynomial.Bivariate.pderiv_one_equivMvPolynomial, Matrix.derivative_det_one_add_X_smul, derivative_rootMultiplicity_of_root, iterate_derivative_mul_X, sumIDeriv_eq_self_add, iterate_derivative_X, Splits.eval_derivative_eq_eval_mul_sum, divByMonic_add_X_sub_C_mul_derivative_divByMonic_eq_derivative, derivative'_apply, mem_support_derivative, card_roots_le_derivative, derivative_eval, iterate_derivative_X_sub_pow, Algebra.discr_powerBasis_eq_norm, derivative_X_sub_C_sq, eval_derivative_of_splits, divRadical_dvd_derivative, aeval_add_of_sq_eq_zero, derivativeFinsupp_apply_toFun, deriv_aeval, iterate_derivative_derivative_mul_X_sq, Derivation.comp_aeval_eq, card_roots_toFinset_le_card_roots_derivative_diff_roots_succ, derivative_X_add_C, hermite_succ, hermite_eq_iterate, iterate_derivative_natCast_mul, bernsteinPolynomial.iterate_derivative_at_1_eq_zero_of_lt, derivative_X_pow_succ, pow_sub_one_dvd_derivative_of_pow_dvd, derivative_X_sub_C_pow, derivWithin, Chebyshev.one_sub_X_sq_mul_derivative_T_eq_poly_in_T, exists_iterate_derivative_eq_factorial_smul, traceForm_dualSubmodule_adjoin, derivativeFinsupp_apply_apply, eval_derivative_eq_eval_mul_sum_of_splits, iterate_derivative_comp_one_sub_X, degree_derivative_lt, derivative_natCast_mul, fderiv_aeval, Splits.eval_derivative_div_eval_of_ne_zero, derivativeFinsupp_derivative, degree_derivative_eq, rootSet_derivative_subset_convexHull_rootSet, Chebyshev.iterate_derivative_T_eval_zero_recurrence, iterate_derivative_X_pow_eq_natCast_mul, Chebyshev.abs_iterate_derivative_T_real_le, lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors, hasFDerivAt, WeierstrassCurve.Affine.derivative_addPolynomial_slope, separable_def', derivative_of_natDegree_zero, lt_rootMultiplicity_iff_isRoot_iterate_derivative, PowerSeries.derivativeFun_coe, iterate_derivative_C, derivative_C_mul_X, eval_iterate_derivative_rootMultiplicity, iterate_derivative_derivative_mul_X, Chebyshev.add_one_mul_self_mul_T_eq_poly_in_T, iterate_derivative_eq_zero, derivative_rootMultiplicity_of_root_of_mem_nonZeroDivisors, iterate_derivative_X_pow_eq_smul, Chebyshev.derivative_U_eval_one, StandardEtalePresentation.toSubmersivePresentation_jacobian, X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic, Lagrange.iterate_derivative_interpolate, pow_sub_dvd_iterate_derivative_pow, hasFDerivAt_aeval, natDegree_derivative_le, iterate_derivative_eq_sum, Chebyshev.iterate_derivative_U_eval_zero_recurrence, sumIDeriv_apply, sylvesterDeriv_updateRow, dvd_derivative_iff, Chebyshev.eval_iterate_derivative_le_of_forall_abs_le_one, eval_derivative_div_eval_of_ne_zero_of_splits, Chebyshev.one_sub_X_sq_mul_iterate_derivative_U_eval, derivative_comp, derivative_sq, one_lt_rootMultiplicity_iff_isRoot_gcd, hasDerivWithinAt_aeval, hasStrictDerivAt_aeval, bernsteinPolynomial.iterate_derivative_succ_at_0_eq_zero, iterate_derivative_eq_zero_of_degree_lt, isRoot_iterate_derivative_of_lt_rootMultiplicity, iterate_derivative_prod_X_sub_C, Chebyshev.iterate_derivative_U_eval_one_recurrence, factorial_mul_shiftedLegendre_eq, Chebyshev.one_sub_X_sq_mul_derivative_derivative_T_eq_poly_in_T, separable_def, iterate_derivative_smul, coeff_iterate_derivative, Chebyshev.T_iterate_derivative_mem_span_T, derivative_eval₂_C, PowerSeries.derivative_coe, aeval_derivative_of_splits, derivative_pow, derivative_prod, Chebyshev.iterate_derivative_U_eval_one, iterate_derivative_C_mul, mkDerivation_one_eq_derivative, iterate_derivative_mul_X_pow, taylor_coeff_one, fderivWithin_aeval, Chebyshev.eval_iterate_derivative_eq_iff_of_bounded, fderivWithin, hasDerivAt, iterate_derivative_sub, Derivation.map_aeval, aeval_derivative_mem_differentIdeal, iterate_derivative_X_pow_eq_C_mul, derivative_X_pow, sumIDeriv_derivative, StandardEtalePair.HasMap.isUnit_derivative_f, IsCoprime.wronskian_eq_zero_iff, KaehlerDifferential.polynomial_D_apply, newtonMap_apply_of_isUnit, exists_derivative_mul_eq_and_isIntegral_coeff, factorial_smul_hasseDeriv, Chebyshev.one_sub_X_sq_mul_iterate_derivative_T_eq_poly_in_T, hasDerivAt_aeval, aeval_root_derivative_of_splits, iterate_derivative_neg, derivative_prod_finset, Differential.deriv_aeval_eq, StandardEtalePair.cond, derivative_sub, hasStrictDerivAt, derivative_monomial_succ, resultant_deriv, Derivation.compAEval_eq, bernsteinPolynomial.derivative_succ, pow_sub_dvd_iterate_derivative_of_pow_dvd, iterate_derivative_X_sub_pow_self, derivative_neg, deriv, hasFDerivWithinAt_aeval, derivative_C_mul_X_pow, derivative_C, derivative_bernoulli_add_one, eval₂_derivative_of_splits, Chebyshev.iterate_derivative_U_eval_one_eq_div, Chebyshev.iterate_derivative_T_eval_one, conductor_mul_differentIdeal, derivative_zero, derivative_X_add_C_sq, one_lt_rootMultiplicity_iff_isRoot_iterate_derivative, newtonMap_apply, Derivation.apply_aeval_eq', natDegree_iterate_derivative, eval_add_of_sq_eq_zero, derivative_X_add_C_pow, hasseDeriv_one, iterate_derivative_mul, aeval_iterate_derivative_of_lt, derivative_map, iterate_derivative_intCast_mul, Lagrange.eval_nodal_derivative_eval_node_eq, Module.Basis.traceDual_powerBasis_eq, derivative_natCast, derivative_bernoulli, bernsteinPolynomial.derivative_zero, iterate_derivative_map, sumIDeriv_apply_of_le, Bivariate.pderiv_one_equivMvPolynomial, bernsteinPolynomial.iterate_derivative_at_0_eq_zero_of_lt, bernsteinPolynomial.iterate_derivative_at_0, Chebyshev.derivative_U_eval_one_eq_div, hasFDerivWithinAt, iterate_derivative_one, natDegree_derivative_lt, Chebyshev.one_sub_X_sq_mul_iterate_derivative_U_eq_poly_in_U, one_lt_rootMultiplicity_iff_isRoot, PowerSeries.trunc_derivativeFun, Matrix.derivative_det_one_add_X_smul_aux, hasDerivWithinAt, PowerSeries.trunc_derivative, bernsteinPolynomial.derivative_succ_aux, derivative_X_sub_C, card_roots_toFinset_le_derivative, iterate_derivative_sum, Chebyshev.one_sub_X_sq_mul_iterate_derivative_T_eval, sumIDeriv_apply_of_lt, degree_derivative_le, Chebyshev.iterate_derivative_T_eval_one_eq_div, isRoot_of_isRoot_iff_dvd_derivative_mul, derivative_one, Chebyshev.derivative_T_eval_one, derivative_apply, mkDerivation_apply, Chebyshev.add_one_mul_T_eq_poly_in_U, derivative_C_mul_X_sq, eval_multiset_prod_X_sub_C_derivative, Chebyshev.T_derivative_mem_span_T, lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors', bernsteinPolynomial.iterate_derivative_at_1, Lagrange.nodalWeight_eq_eval_derivative_nodal, derivative_intCast, derivative_add, Derivation.apply_aeval_eq, PowerSeries.trunc_derivative'
|