| Metric | Count |
|---|
DefinitionsIsRoot, decidable, comp, compRingHom, eval, evalRingHom, evalā, evalāAddMonoidHom, evalāRingHom, evalāRingHom', map, mapRingHom | 12 |
TheoremsC_comp, C_mul_comp, def, dvd, eq_zero, X_comp, X_pow_comp, add_comp, associated_map_map, coe_compRingHom, coe_compRingHom_apply, coe_evalRingHom, coe_evalāRingHom, coe_mapRingHom, comp_C, comp_X, comp_assoc, comp_eq_sum_left, comp_one, comp_zero, eval_C, eval_C_mul, eval_X, eval_X_pow, eval_add, eval_comp, eval_dvd, eval_eq_sum, eval_eq_zero_of_dvd_of_eval_eq_zero, eval_finset_sum, eval_geom_sum, eval_intCast, eval_listSum, eval_list_prod, eval_map, eval_map_apply, eval_monomial, eval_mul, eval_mul_X, eval_mul_X_pow, eval_multisetSum, eval_multiset_prod, eval_natCast, eval_natCast_mul, eval_neg, eval_ofNat, eval_one, eval_pow, eval_prod, eval_sub, eval_sum, eval_surjective, eval_zero, evalāAddMonoidHom_apply, evalāRingHom'_apply, evalā_C, evalā_X, evalā_X_mul, evalā_X_pow, evalā_add, evalā_at_apply, evalā_at_intCast, evalā_at_natCast, evalā_at_ofNat, evalā_at_one, evalā_congr, evalā_def, evalā_dvd, evalā_eq_eval_map, evalā_eq_sum, evalā_eq_zero_of_dvd_of_evalā_eq_zero, evalā_finset_prod, evalā_finset_sum, evalā_id, evalā_list_prod, evalā_list_prod_noncomm, evalā_list_sum, evalā_monomial, evalā_mul, evalā_mul_C', evalā_mul_X, evalā_mul_eq_zero_of_left, evalā_mul_eq_zero_of_right, evalā_mul_noncomm, evalā_multiset_prod, evalā_multiset_sum, evalā_natCast, evalā_neg, evalā_ofFinsupp, evalā_ofNat, evalā_one, evalā_pow, evalā_sub, evalā_sum, evalā_zero, intCast_comp, isRoot_comp, isRoot_prod, list_prod_comp, mapRingHom_comp_C, map_C, map_X, map_add, map_comp, map_dvd, map_intCast, map_list_prod, map_monomial, map_mul, map_multiset_prod, map_natCast, map_neg, map_ofNat, map_one, map_pow, map_prod, map_sub, map_sum, map_zero, monomial_comp, mul_X_add_natCast_comp, mul_X_comp, mul_X_pow_comp, mul_X_sub_intCast_comp, mul_comp, mul_comp_neg_X, multiset_prod_comp, natCast_comp, natCast_mul_comp, neg_comp, not_isRoot_C, ofNat_comp, one_comp, pow_comp, prod_comp, root_X_sub_C, root_mul, root_mul_left_of_isRoot, root_mul_right_of_isRoot, root_or_root_of_root_mul, sub_comp, sum_comp, zero_comp | 143 |
| Total | 155 |
| Name | Category | Theorems |
|---|
IsRoot š | MathDef | 65 mathmath: mul_div_eq_iff_isRoot, mul_divByMonic_eq_iff_isRoot, root_X_sub_C, eventually_atBot_not_isRoot, Matrix.mem_spectrum_iff_isRoot_charpoly, not_isRoot_C, HenselianLocalRing.is_henselian, roots_eq_zero_iff_isRoot_eq_bot, Irreducible.subsingleton_isRoot, num_isRoot_scaleRoots_of_aeval_eq_zero, Real.Polynomial.isRoot_cos_pi_div_five, HenselianRing.is_henselian, isRoot_of_aeval_algebraMap_eq_zero, zero_isRoot_of_coeff_zero_eq_zero, Module.End.hasEigenvalue_iff_isRoot_charpoly, IsRoot.def, Irreducible.isRoot_eq_bot_of_natDegree_ne_one, isRoot_cyclotomic_iff_charZero, lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors, IsRealClosed.exists_isRoot_of_odd_natDegree, rootMultiplicity_pos, lt_rootMultiplicity_iff_isRoot_iterate_derivative, Complex.exists_root, isRoot_gcd_iff_isRoot_left_right, LinearMap.hasEigenvalue_zero_tfae, eventually_atTop_not_isRoot, IsCyclotomicExtension.zeta_isRoot, Module.End.isRoot_of_hasEigenvalue, subsingleton_isRoot_of_natDegree_eq_one, one_lt_rootMultiplicity_iff_isRoot_gcd, isRoot_iterate_derivative_of_lt_rootMultiplicity, exists_root_of_degree_eq_one, IsAlgClosed.exists_root, WittVector.RecursionMain.succNthVal_spec, Irreducible.not_isRoot_of_natDegree_ne_one, isRoot_of_mem_roots, mem_roots, mem_roots', zero_isRoot_iff_coeff_zero_eq_zero, Module.End.hasEigenvalue_iff_isRoot, WittVector.RecursionMain.root_exists, LinearRecurrence.geom_sol_iff_root_charPoly, root_mul, isRoot_prod, isRoot_map_iff, roots_eq_zero_iff_eq_zero_or_isRoot_eq_bot, one_lt_rootMultiplicity_iff_isRoot_iterate_derivative, IsPrimitiveRoot.pow_isRoot_minpoly, isRoot_comp, isRoot_cyclotomic_prime_pow_mul_iff_of_charP, IsSepClosed.exists_root, dvd_iff_isRoot, Module.End.mem_spectrum_iff_isRoot_charpoly, LinearMap.not_hasEigenvalue_zero_tfae, rootMultiplicity_pos', one_lt_rootMultiplicity_iff_isRoot, isRoot_of_unity_iff, isRoot_of_isRoot_iff_dvd_derivative_mul, isRoot_cyclotomic_iff, eventually_no_roots, finite_setOf_isRoot, lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors', AdjoinRoot.isRoot_root, isRoot_of_evalā_map_eq_zero, IsPrimitiveRoot.isRoot_cyclotomic
|
comp š | CompOp | 129 mathmath: Splits.comp_of_degree_le_one_of_invertible, dickson_one_one_mul, comp_assoc, rootMultiplicity_eq_rootMultiplicity, rootMultiplicity_eq_natTrailingDegree, derivative_comp_one_sub_X, PolynomialModule.comp_smul, descPochhammer_succ_comp_X_sub_one, irreducible_comp, Chebyshev.S_eq_U_comp_half_mul_X, comp_neg_X_eq_zero_iff, chebyshev_U_eq_dickson_two_one, pow_comp, zero_comp, eval_divByMonic_eq_trailingCoeff_comp, Chebyshev.S_comp_two_mul_X, coe_compRingHom_apply, dvd_comp_X_add_C_iff, X_comp, dvd_comp_C_mul_X_add_C_iff, Monic.comp_X_sub_C, Splits.comp_of_map_degree_le_one, expand_eq_comp_X_pow, ascPochhammer_succ_comp_X_add_one, minpoly.sub_algebraMap, natDegree_comp, Matrix.charpoly_sub_scalar, splits_iff_comp_splits_of_natDegree_eq_one, aeval_comp, degree_comp, comp_C_mul_X_eq_zero_iff, ascPochhammer_mul, dickson_one_one_comp_comm, Chebyshev.T_mul, Splits.comp_X_sub_C, comp_C, splits_iff_comp_splits_of_degree_eq_one, natDegree_comp_eq_of_mul_ne_zero, bernsteinPolynomial.flip', list_prod_comp, multiset_prod_comp, sum_comp, taylor_apply, iterate_derivative_comp_one_sub_X, IsPrimitiveRoot.minpoly_sub_one_eq_cyclotomic_comp, Splits.comp_X_add_C, iterate_comp_eval, bernsteinPolynomial.flip, intCast_comp, Gal.restrictComp_surjective, comp_eq_zero_iff, descPochhammer_eq_ascPochhammer, comp_C_mul_X_coeff, descPochhammer_succ_left, comp_neg_X_leadingCoeff_eq, descPochhammer_mul, mul_comp_neg_X, Monic.comp, mul_X_pow_comp, bernoulli_comp_one_add_X, comp_X, derivative_comp, add_comp, natDegree_iterate_comp, leadingCoeff_comp, cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt, eval_comp, minpoly.add_algebraMap, C_comp, comp_one, coe_compRingHom, Gal.splits_in_splittingField_of_comp, dickson_one_one_eq_chebyshev_T, Splits.comp_of_natDegree_le_one, ascPochhammer_eval_comp, chebyshev_T_eq_dickson_one_one, one_comp, IsMonicOfDegree.comp, Monic.comp_X_add_C, mul_X_add_natCast_comp, Chebyshev.C_comp_two_mul_X, comp_eq_aeval, ofNat_comp, smeval_comp, natCast_comp, prod_comp, degree_comp_neg_X, geom_sum_X_comp_X_add_one_eq_sum, LinearMap.charpoly_sub_smul, minpoly.neg, comp_zero, dvd_comp_neg_X_iff, dickson_two_one_eq_chebyshev_U, C_mul_comp, mul_X_comp, Chebyshev.C_eq_two_mul_T_comp_half_mul_X, iterate_comp_evalā, Chebyshev.T_eq_half_mul_C_comp_two_mul_X, mul_comp, comp_eq_sum_left, dvd_comp_X_sub_C_iff, isRoot_comp, cyclotomic_comp_X_add_one_isEisensteinAt, Chebyshev.C_mul, mul_X_sub_intCast_comp, evalā_comp, map_comp, neg_comp, comp_X_add_C_eq_zero_iff, Splits.comp_of_natDegree_le_one_of_monic, natCast_mul_comp, Splits.comp_neg_X, natDegree_comp_le, X_pow_comp, bernoulli_comp_one_sub_X, coeff_comp_degree_mul_degree, bernoulli_comp_neg_X, comp_neg_X_comp_neg_X, ascPochhammer_succ_left, Splits.comp_of_degree_le_one_of_monic, smul_comp, monomial_comp, neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq, Splits.comp_of_natDegree_le_one_of_invertible, evalā_comp', sub_comp, X_sub_C_pow_dvd_iff, Monic.neg_one_pow_natDegree_mul_comp_neg_X, Splits.comp_of_degree_le_one
|
compRingHom š | CompOp | 2 mathmath: coe_compRingHom_apply, coe_compRingHom
|
eval š | CompOp | 478 mathmath: fderiv, ascPochhammer_ne_zero_eval_zero, Chebyshev.isExtrOn_T_real_iff, Chebyshev.S_two_mul_complex_cos, differentiableWithinAt, taylor_eval, Lagrange.eval_iterate_derivative_eq_sum, mahlerMeasure_def_of_ne_zero, Derivation.apply_eval_eq, ordinaryHypergeometric_sum_eq, bernoulli_eval_one_sub, eval_multiset_prod, Chebyshev.U_eval_zero, bernsteinPolynomial.eval_at_1, isEquivalent_atBot_div, Lagrange.eval_interpolate_not_at_node', resultant_X_add_C_right, Nat.cast_factorial, Lagrange.nodalWeight_eq_eval_nodal_erase_inv, Nat.cast_choose_eq_ascPochhammer_div, eval_minpolyDiv_self, Chebyshev.U_eval_one, Chebyshev.complex_ofReal_eval_S, expNegInvGlue.hasDerivAt_polynomial_eval_inv_mul, aeval_algebraMap_apply_eq_algebraMap_eval, HurwitzZeta.cosZeta_two_mul_nat', Chebyshev.algebraMap_eval_U, one_le_pow_mul_abs_eval_div, eval_prod, div_tendsto_atTop_leadingCoeff_div_of_degree_eq, mem_roots_sub_C', ascPochhammer_succ_eval, div_tendsto_atBot_leadingCoeff_div_of_degree_eq, eval_det_add_X_smul, bernoulli_eval_one, FirstOrder.Field.realize_genericMonicPolyHasRoot, ascPochhammer_eval_one, continuous, cyclotomic_pos', isCoveringMapOn_eval, HurwitzZeta.cosZeta_two_mul_nat, eval_map, Splits.eval_derivative, evalā_hom, sub_one_pow_totient_le_cyclotomic_eval, toContinuousMap_apply, coeff_zero_eq_eval_zero, eval_minpolyDiv_of_aeval_eq_zero, Lagrange.eval_interpolate_not_at_node, Chebyshev.eval_T_real_node, Chebyshev.complex_ofReal_eval_T, dvd_iterate_derivative_pow, map_sub_roots_sprod_eq_prod_map_eval, Chebyshev.eval_T_real_eq_neg_one_iff, Splits.eval_root_derivative, differentiable_descPochhammer_eval, bernoulli_succ_eval, Nat.cast_ascFactorial, div_tendsto_zero_iff_degree_lt, Chebyshev.integral_T_real_mul_self_measureT_of_ne_zero, Chebyshev.T_eval_zero, aeval_iterate_derivative_self, Chebyshev.eval_T_real_mem_Icc, eval_C, Chebyshev.iterate_derivative_T_eval_one_recurrence, evalā_id, eval_divByMonic_eq_trailingCoeff_comp, Chebyshev.isLocalMin_T_real, bernoulli_eval_zero, abs_div_tendsto_atTop_of_degree_gt, minpolyDiv_eval_eq_zero_of_ne_of_aeval_eq_zero, Matrix.derivative_det_one_add_X_smul, resultant_X_sub_C_right, cyclotomic.eval_apply_ofReal, descPochhammer_ne_zero_eval_zero, tendsto_atTop_iff_leadingCoeff_nonneg, Lagrange.coeff_eq_sum, cyclotomic_eval_lt_add_one_pow_totient, Splits.eval_derivative_eq_eval_mul_sum, map_rootOfSplits, eval_surjective, bernoulli_eval_one_add, exists_root_of_splits', Chebyshev.T_eval_two_mul_zero, isEquivalent_atTop_lead, ascPochhammer_nat_eq_descFactorial, eval_natCast_map, isLittleO_atTop_of_degree_lt, continuousWithinAt, Matrix.det_eval_matrixOfPolynomials_eq_det_vandermonde, monotoneOn_descPochhammer_eval, Lagrange.eq_interpolate_iff, eval_X, derivative_eval, abs_div_tendsto_atBot_atTop_of_degree_gt, Chebyshev.complex_ofReal_eval_C, Chebyshev.T_eval_neg, Matrix.det_one_add_smul, eval_pow, abs_div_tendsto_atTop_atTop_of_degree_gt, div_tendsto_atTop_of_degree_gt', FirstOrder.Field.lift_genericMonicPoly, Chebyshev.T_real_cos, descPochhammer_eval_div_factorial_le_sum_choose, Lagrange.eval_nodal_at_node, eval_X_pow, eval_derivative_of_splits, tendsto_atBot_iff_leadingCoeff_nonpos, ascPochhammer_eval_zero, mem_span_C_X_sub_C_X_sub_C_iff_eval_eval_eq_zero, Chebyshev.aeval_T, Chebyshev.U_eval_neg_one, eval_natCast, isClosedMap_eval, ofReal_eval, abs_tendsto_atTop_iff, MvPolynomial.eval_eq_eval_mv_eval', isUnit_iff', Module.reflection_mul_reflection_pow_apply, tendsto_abv_atTop, sub_one_pow_totient_lt_natAbs_cyclotomic_eval, resultant_eq_prod_eval, div_tendsto_atBot_zero_of_degree_lt, sub_one_lt_natAbs_cyclotomic_eval, abs_tendsto_atTop, descPochhammer_eval_cast, HurwitzZeta.hurwitzZeta_neg_nat, Chebyshev.isLocalMax_T_real, sum_range_pow_eq_bernoulli_sub, comp_C, bernsteinPolynomial.iterate_derivative_at_1_eq_zero_of_lt, eval_monomial_one_add_sub, Chebyshev.S_two_mul_real_cos, fwdDiff_iter_degree_add_one_eq_zero, FiniteField.card_image_polynomial_eval, PadicInt.norm_ascPochhammer_le, cfc_map_polynomial, ordinaryHypergeometricSeries_apply_eq', IsRoot.def, derivWithin, Chebyshev.T_eval_one, intervalIntegrable_mahlerMeasure, preHilbertPoly_eq_choose_sub_add, Lagrange.eval_nodal, abs_tendsto_atBot_iff, continuousOn, bernoulli_eval_neg, Chebyshev.T_complex_cosh, Chebyshev.C_two_mul_complex_cosh, eval_derivative_eq_eval_mul_sum_of_splits, evalEvalRingHom_apply, Chebyshev.abs_eval_T_real_le_one, Splits.eval_derivative_div_eval_of_ne_zero, ascPochhammer_nat_eq_natCast_descFactorial, Module.End.aeval_apply_of_hasEigenvector, eval_dvd, descPochhammer_eval_le_sum_descFactorial, HurwitzZeta.hurwitzZetaOdd_neg_two_mul_nat, exists_polynomial_near_of_continuousOn, iterate_comp_eval, Module.reflection_mul_reflection_pow, isBigO_atBot_of_degree_le, monotoneOn_deriv_descPochhammer_eval, Lagrange.eval_basisDivisor_right, eval_homogenize, quotientSpanXSubCAlgEquiv_mk, isProperMap_eval, eval_mul, eval_list_prod, Chebyshev.algebraMap_eval_C, Chebyshev.S_two_mul_real_cosh, Chebyshev.iterate_derivative_T_eval_zero_recurrence, Chebyshev.one_lt_abs_eval_T_real, fwdDiff_iter_eq_zero_of_degree_lt, Matrix.eval_charpolyRev, hasFDerivAt, hasSum_one_div_nat_pow_mul_cos, ascPochhammer_eval_eq_zero_iff, Chebyshev.aeval_S, cyclotomic_pos_and_nonneg, algebraMap_pi_self_eq_eval, evalā_at_natCast, Lagrange.eq_interpolate, map_sub_sprod_roots_eq_prod_map_eval, isBigO_of_degree_le, expNegInvGlue.tendsto_polynomial_inv_mul_zero, eval_intCast_map, Lagrange.leadingCoeff_eq_sum, Asymptotics.SuperpolynomialDecay.mul_polynomial, Splits.eval_eq_prod_roots_of_monic, smul_eval_smul, comp_eq_zero_iff, taylor_coeff_zero, ordinaryHypergeometric_eq_tsum, tendsto_norm_atTop, exists_forall_norm_le, descPochhammer_nonneg, isEquivalent_atTop_div, Chebyshev.U_eval_zero_of_odd, Nat.cast_choose_eq_descPochhammer_div, resultant_X_sub_C_pow_left, convexOn_descPochhammer_eval, eval_iterate_derivative_rootMultiplicity, SModEq.eval, logMahlerMeasure_def, Chebyshev.C_eval_two, Chebyshev.integral_eval_T_real_measureT_zero, eval_zero, div_tendsto_atBot_of_degree_gt, eval_one_cyclotomic_prime_pow, eval_eq_prod_roots_sub_of_splits_id, Chebyshev.derivative_U_eval_one, resultant_X_sub_C_pow_right, X_sub_C_dvd_sub_C_eval, spectrum.exists_mem_of_not_isUnit_aeval_prod, isEquivalent_atBot_lead, coeff_mul_invOneSubPow_eq_hilbertPoly_eval, HurwitzZeta.hurwitzZetaEven_one_sub_two_mul_nat, Chebyshev.iterate_derivative_U_eval_zero_recurrence, ordinaryHypergeometricSeries_apply_eq, Chebyshev.U_real_cos, evalā_at_intCast, spectrum.map_polynomial_aeval_of_nonempty, expand_zero, HurwitzZeta.sinZeta_two_mul_nat_add_one', eval_one_map, div_tendsto_leadingCoeff_div_of_degree_eq, LinearMap.eval_charpoly, eval_derivative_div_eval_of_ne_zero_of_splits, Chebyshev.one_sub_X_sq_mul_iterate_derivative_U_eval, Splits.eval_eq_prod_roots, Chebyshev.isMinOn_T_real, eval_C_X_evalā_map_C_X, IsPrimitiveRoot.sub_one_norm_eq_eval_cyclotomic, eval_finset_sum, sub_dvd_eval_sub, Chebyshev.isLocalExtr_T_real_iff, Module.reflection_mul_reflection_pow_apply_self, ascPochhammer_nat_eval_succ, tendsto_atBot_of_leadingCoeff_nonpos, MulSemiringAction.eval_charpoly, Algebra.Norm.Transitivity.eval_zero_comp_det, tendsto_nhds_iff, mem_roots_sub_C, descPochhammer_int_eq_ascFactorial, differentiableOn, Chebyshev.U_eval_two_mul_zero, eval_intCast, AnalyticOnNhd.eval_polynomial, cyclotomic.eval_apply, evalā_at_one, resultant_X_add_C_left, ascPochhammer_eval_neg_coe_nat_of_lt, eval_comp, Chebyshev.integral_eval_T_real_mul_eval_T_real_measureT, bernsteinPolynomial.iterate_derivative_succ_at_0_eq_zero, Lagrange.eval_basis_of_ne, eval_map_apply, Chebyshev.U_complex_cosh, eval_det, sum_sq_norm_coeff_eq_circleAverage, cfc_eval_C, div_tendsto_atTop_of_degree_gt, Chebyshev.iterate_derivative_U_eval_one_recurrence, descPochhammer_eval_eq_descFactorial, Lagrange.eval_basisDivisor_left_of_ne, eval_one_cyclotomic_not_prime_pow, ascPochhammer_pos, isBoundedUnder_abs_atBot_iff, WeierstrassCurve.Affine.equation_add_iff, eval_listSum, eval_mul_X_pow, spectrum.subset_polynomial_aeval, eval_one_cyclotomic_prime, Chebyshev.isMaxOn_T_real, comp_one, eval_eq_prod_roots_sub_of_monic_of_splits_id, Chebyshev.T_complex_cos, eval_natCast_mul, Chebyshev.algebraMap_eval_T, aeval_derivative_of_splits, exists_root_of_splits, eval_zero_map, eval_eq_sum_range', LindemannWeierstrass.integral_exp_mul_eval, eval_sumIDeriv_of_pos, aeval_continuousMap_apply, Chebyshev.U_eval_neg, Chebyshev.integral_eval_T_real_measureT_of_ne_zero, expNegInvGlue.continuous_polynomial_eval_inv_mul, cfc_polynomial, Chebyshev.iterate_derivative_U_eval_one, ascPochhammer_eval_comp, FiniteField.exists_root_sum_quadratic, HurwitzZeta.sinZeta_two_mul_nat_add_one, tendsto_atTop_of_leadingCoeff_nonneg, Chebyshev.S_two_mul_complex_cosh, descPochhammer_eval_coe_nat_of_lt, spectrum.map_polynomial_aeval_of_degree_pos, mirror_eval_one, taylor_coeff_one, Chebyshev.C_eval_neg_two, Matrix.eval_charpoly, fderivWithin, hasDerivAt, pow_le_descPochhammer_eval, Chebyshev.T_real_cosh, matPolyEquiv_eval_eq_map, eval_eq_sum_degreeLTEquiv, modByMonic_X_sub_C_eq_C_eval, Chebyshev.T_eval_zero_of_even, eval_eq_sum, aeval_sumIDeriv_eq_eval, eval_add, isBoundedUnder_abs_atTop_iff, leval_apply, isOpenQuotientMap_eval, descPochhammer_pos, Chebyshev.one_le_abs_eval_T_real, Module.reflection_mul_reflection_zpow_apply_self, expNegInvGlue.contDiff_polynomial_eval_inv_mul, aeval_ofReal, aeval_root_derivative_of_splits, Chebyshev.aeval_C, C_eq_or_isOpenQuotientMap_eval, MvPolynomial.eval_toMvPolynomial, taylor_eval_sub, Chebyshev.aeval_U, cyclotomic_nonneg, hasSum_one_div_nat_pow_mul_sin, mod_X_sub_C_eq_C_eval, div_tendsto_atBot_zero_iff_degree_lt, Chebyshev.complex_ofReal_eval_U, PolynomialModule.eval_smul, hasStrictDerivAt, Module.reflection_mul_reflection_zpow_apply, descPochhammer_eval_eq_ascPochhammer, descPochhammer_eval_eq_prod_range, Chebyshev.one_lt_eval_T_real, Chebyshev.U_complex_cos, differentiableAt, ascPochhammer_zero_eval_zero, ascPochhammer_nat_eq_natCast_ascFactorial, eval_one, abs_tendsto_atBot, PolynomialModule.comp_eval, modByMonic_X, map_rootOfSplits', eval_sum, Chebyshev.C_two_mul_complex_cos, ascPochhammer_eval_succ, eval_mul_X_sub_C, MvPolynomial.polynomial_eval_evalā, div_tendsto_atTop_zero_of_degree_lt, IsAlgClosed.eval_surjective, Chebyshev.one_le_eval_T_real, comp_zero, deriv, div_tendsto_zero_of_degree_lt, Real.iter_deriv_rpow_const, fwdDiff_iter_degree_eq_factorial, Chebyshev.eval_T_real_eq_one_iff, matPolyEquiv_symm_map_eval, evalā_at_apply, Chebyshev.U_real_cosh, Chebyshev.algebraMap_eval_S, evalā_derivative_of_splits, bernsteinPolynomial.eval_at_0, abs_isBoundedUnder_iff, ascPochhammer_smeval_eq_eval, Chebyshev.iterate_derivative_U_eval_one_eq_div, Splits.exists_eval_eq_zero, eval_map_algebraMap, Algebra.Norm.Transitivity.eval_zero_det_det, Chebyshev.iterate_derivative_T_eval_one, eval_eq_sum_range, ascPochhammer_eval_cast, Lagrange.eval_interpolate_at_node, matPolyEquiv_eval, eval_smul, Lagrange.interpolate_poly_eq_self, taylor_coeff, eval_ofNat, cyclotomic_eval_le_add_one_pow_totient, eval_neg, expand_eval, continuousAt, descPochhammer_succ_eval, Chebyshev.integral_eval_T_real_mul_eval_T_real_measureT_of_ne, eval_eq_smeval, evalEval_map_C, isRoot_comp, continuous_descPochhammer_eval, eval_mul_X, differentiable, Chebyshev.S_eval_two, IsRoot.eq_zero, deriv_descPochhammer_eval_eq_sum_prod_range_erase, coe_aeval_eq_eval, Asymptotics.SuperpolynomialDecay.polynomial_mul, sub_one_pow_totient_lt_cyclotomic_eval, Chebyshev.one_lt_negOnePow_mul_eval_T_real, eval_add_of_sq_eq_zero, isLittleO_atBot_of_degree_lt, smul_eval, eval_multisetSum, Chebyshev.integral_eval_T_real_mul_self_measureT_zero, ascPochhammer_nat_eq_ascFactorial, Chebyshev.one_le_negOnePow_mul_eval_T_real, Chebyshev.T_eval_neg_one, Chebyshev.isLocalExtr_T_real, evalā_at_ofNat, Lagrange.eval_nodal_derivative_eval_node_eq, Chebyshev.isExtrOn_T_real, resultant_X_sub_C_left, map_mapRingHom_eval_map, AnalyticOn.eval_polynomial, descPochhammer_zero_eval_zero, dickson_one_one_eval_add_inv, descPochhammer_eval_zero, eval_rootOfSplits, tendsto_div_exp_atTop, bernsteinPolynomial.iterate_derivative_at_0_eq_zero_of_lt, bernsteinPolynomial.iterate_derivative_at_0, Chebyshev.derivative_U_eval_one_eq_div, hasFDerivWithinAt, MvPolynomial.optionEquivLeft_elim_eval, Lagrange.eval_basis_self, preimage_eval_singleton, map_mapRingHom_eval_map_eval, polynomial_smul_apply, Chebyshev.S_eval_neg_two, Chebyshev.abs_eval_T_real_le_one_iff, eval_sub, cfc_eval_X, spectrum.map_polynomial_aeval, evalEval_C, evalā_eq_eval_map, map_evalRingHom_eval, scaleRoots_eval_mul, div_tendsto_atTop_zero_iff_degree_lt, expNegInvGlue.differentiable_polynomial_eval_inv_mul, Matrix.derivative_det_one_add_X_smul_aux, hasDerivWithinAt, bernoulli_three_eval_one_quarter, Matrix.eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials, prodXSubSMul.eval, cyclotomic_pos, Chebyshev.one_sub_X_sq_mul_iterate_derivative_T_eval, eval_smul', ascPochhammer_evalā, Chebyshev.iterate_derivative_T_eval_one_eq_div, Chebyshev.derivative_T_eval_one, LindemannWeierstrass.hasDerivAt_cexp_mul_sumIDeriv, Module.reflection_mul_reflection_mul_reflection_pow_apply_self, coe_evalRingHom, eval_C_mul, Module.reflection_mul_reflection_mul_reflection_zpow_apply_self, Module.reflection_mul_reflection_zpow, Chebyshev.C_two_mul_real_cos, ascPochhammer_eval_neg_eq_descPochhammer, Nat.cast_descFactorial, Chebyshev.abs_eval_T_real_eq_one_iff, div_tendsto_atBot_of_degree_gt', Chebyshev.U_eval_zero_of_even, Chebyshev.eval_T_real_cos_int_mul_pi_div, eval_multiset_prod_X_sub_C_derivative, bernsteinPolynomial.iterate_derivative_at_1, Lagrange.nodalWeight_eq_eval_derivative_nodal, isBigO_atTop_of_degree_le, eval_geom_sum, Chebyshev.C_two_mul_real_cosh, Lagrange.eval_basis_not_at_node, eval_monomial, factorial_mul_ascPochhammer, Chebyshev.T_eval_zero_of_odd, aeval_sumIDeriv_of_pos, MvPolynomial.eval_polynomial_eval_finSuccEquiv
|
evalRingHom š | CompOp | 14 mathmath: ker_evalRingHom, AdjoinRoot.evalEval_apply, MvPolynomial.eval_comp_toMvPolynomial, evalEvalRingHom_eq, LieAlgebra.engel_isBot_of_isMin.lieCharpoly_map_eval, evalRingHom_mapMatrix_comp_polyToMatrix, evalRingHom_mapMatrix_comp_compRingEquiv, evalRingHom_zero, evalā_evalRingHom, eval_C_X_comp_evalā_map_C_X, MvPolynomial.polynomial_eval_evalā, coe_aeval_eq_evalRingHom, map_evalRingHom_eval, coe_evalRingHom
|
evalā š | CompOp | 106 mathmath: evalā_C_X_eq_coe, evalā_one_cyclotomic_prime, evalā_finset_prod, evalā_multiset_prod, evalā_intCastRingHom_X, evalā_minpolyDiv_self, evalā_homogenize_of_eq_one, tendsto_abv_evalā_atTop, MvPolynomial.pUnitAlgEquiv_symm_apply, eval_map, FixedPoints.minpoly.evalā', evalā_hom, evalā_mul_X, evalā_X_pow, PowerSeries.evalā_coe, evalā_one, evalā_restriction, evalā_zero, evalā_id, scaleRoots_evalā_mul, evalā_reflect_eq_zero_iff, evalā_ofFinsupp, evalā_monomial, IsAlgClosed.exists_evalā_eq_zero_of_injective, evalā_finset_sum, evalā_list_sum, hom_evalā, MvPolynomial.evalā_const_pUnitAlgEquiv_symm, evalā_mul', evalā_list_prod, evalā_dvd, evalā_natCast, scaleRoots_evalā_mul_of_commute, mem_roots_map_of_injective, evalā_sum, evalā_reflect_mul_pow, evalā_C_X, evalā_sub, evalā_map, evalā_at_natCast, eval_unique, int_evalā_eq, aeval_def, evalā_def, evalā_at_intCast, evalā_mul_C', eval_C_X_evalā_map_C_X, evalā_mul, evalā_at_one, evalā_evalRingHom, IsAlgClosed.exists_evalā_eq_zero, evalā_congr, LaurentPolynomial.evalā_toLaurent, evalā_at_zero, AdjoinRoot.evalā_root, derivative_evalā_C, ascPochhammer_eval_comp, coe_expand, MvPolynomial.evalā_const_pUnitAlgEquiv, evalāRingHom'_apply, evalā_pow, root_gcd_iff_root_left_right, IsSepClosed.exists_evalā_eq_zero_of_injective, evalā_X, evalā_X_mul, evalāAddMonoidHom_apply, mem_roots_map, polyEquivTensor_apply, MvPolynomial.evalā_pUnitAlgEquiv_symm, evalā_neg, evalā_C, evalā_pow', evalā_at_apply, integralNormalization_evalā_leadingCoeff_mul_of_commute, iterate_comp_evalā, algHom_evalā_algebraMap, evalā_multiset_sum, PowerSeries.evalā_trunc_eq_sum_range, evalā_eq_sum_range, evalā_ofNat, evalā_one_cyclotomic_prime_pow, evalā_reverse_mul_pow, evalā_comp, evalā_at_ofNat, ringHom_evalā_intCastRingHom, evalāAlgHom'_apply, evalā_eq_sum, evalā_eq_sum_range', evalā_smul, MvPolynomial.evalā_pUnitAlgEquiv, continuous_evalā, coe_evalāRingHom, evalā_eq_eval_map, FixedPoints.minpoly.evalā, ascPochhammer_evalā, evalā_list_prod_noncomm, IsSepClosed.exists_evalā_eq_zero, evalā_evalāRingHom_apply, evalā_mul_noncomm, evalā_comp', RatFunc.eval_algebraMap, evalā_algebraMap_X, integralNormalization_evalā_leadingCoeff_mul, evalā_reverse_eq_zero_iff, evalā_add, evalā_smulOneHom_eq_smeval
|
evalāAddMonoidHom š | CompOp | 1 mathmath: evalāAddMonoidHom_apply
|
evalāRingHom š | CompOp | 7 mathmath: evalāRingHom_evalāRingHom, AdjoinRoot.evalEval_apply, evalEvalRingHom_eq, eval_C_X_comp_evalā_map_C_X, coe_evalāRingHom, Ideal.evalā_C_mk_eq_zero, evalā_evalāRingHom_apply
|
evalāRingHom' š | CompOp | 1 mathmath: evalāRingHom'_apply
|
map š | CompOp | 374 mathmath: degree_map_le, NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply', WeierstrassCurve.map_Ļā, WeierstrassCurve.baseChange_ĪØSq, map_dickson, nextCoeff_map, map_one, homogenize_map, WeierstrassCurve.map_ĪØāSq, Matrix.charpoly.univ_map_map, HurwitzZeta.cosZeta_two_mul_nat', Ideal.exists_mem_span_singleton_map_residueField_eq, WeierstrassCurve.map_Ļ, one_le_pow_mul_abs_eval_div, eq_rootMultiplicity_map, card_roots_le_map, lifts_and_degree_eq_and_monic, leadingCoeff_map', IsPrimitiveRoot.minpoly_dvd_pow_mod, PolynomialModule.map_smul, fiberEquivQuotient_tmul, aeval_map_algebraMap, map_mul, WeierstrassCurve.baseChange_preĪØ, Matrix.charpoly_map, map_div, monic_map_iff, coeff_map, HurwitzZeta.cosZeta_two_mul_nat, WeierstrassCurve.map_ĪØ, sum_smul_minpolyDiv_eq_X_pow, eval_map, IsDistinguishedAt.map_eq_X_pow, Normal.splits', PowerBasis.quotientEquivQuotientMinpolyMap_apply, sumIDeriv_map, map_injective_iff, WeierstrassCurve.baseChange_preĪØā, map_modByMonic, Splits.roots_map_of_injective, matPolyEquiv_map_smul, roots_map_of_injective_of_card_eq_natDegree, ConjRootClass.minpoly.map_eq_prod, WeierstrassCurve.Affine.map_polynomialY, map_dvd, splits_map_iff, count_map_roots, map_list_prod, IsPrimitive.isUnit_iff_isUnit_map_of_injective, IsPrimitiveRoot.is_roots_of_minpoly, map_surjective, UniversalCoprimeFactorizationRing.homEquiv_comp_snd, isUnit_map, AdjoinRoot.quotEquivQuotMap_symm_apply_mk, eval_natCast_map, WeierstrassCurve.baseChange_ĪØāSq, int_coeff_of_cyclotomic', map_expand, mapEquiv_symm_apply, Gal.restrictDvd_def, unique_int_coeff_of_cycl, map_mod, integralNormalization_map, reflect_map, Cubic.splits_iff_card_roots, card_roots_map_le_degree, natDegree_map_eq_iff, IsAlgClosed.splits_codomain, le_rootMultiplicity_map, IsLocalization.integerNormalization_map_to_map, WeierstrassCurve.Affine.map_linePolynomial, PowerBasis.quotientEquivQuotientMinpolyMap_apply_mk, WeierstrassCurve.baseChange_preĪØ', Normal.splits, degree_map_eq_of_isUnit_leadingCoeff, map_monomial, WeierstrassCurve.baseChange_Ļā, WeierstrassCurve.Affine.baseChange_negPolynomial, IsAlgClosed.card_roots_map_eq_natDegree_of_isUnit_leadingCoeff, MvPolynomial.eval_eq_eval_mv_eval', PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply_mk, LinearMap.polyCharpoly_baseChange, AdjoinRoot.mul_div_root_cancel, minpoly.natSepDegree_eq_one_iff_eq_X_sub_C_pow, LinearMap.polyCharpolyAux_map_eval, aroots_map, IsNormalClosure.splits, mem_roots_map_of_injective, AdjoinRoot.aeval_eq_of_algebra, natDegree_map, minpoly.map_eq_of_isSeparable_of_isPurelyInseparable, HurwitzZeta.hurwitzZeta_neg_nat, minpoly.frobenius_of_isSeparable, map_pow, int_cyclotomic_rw, map_taylor, LieAlgebra.engel_isBot_of_isMin.lieCharpoly_map_eval, UniversalCoprimeFactorizationRing.homEquiv_comp_fst, IsPrimitive.irreducible_iff_irreducible_map_fraction_map, leadingCoeff_map_eq_of_isUnit_leadingCoeff, bUnion_roots_finite, natSepDegree_map, WeierstrassCurve.Affine.map_negPolynomial, IsCyclotomicExtension.splits_cyclotomic, count_map_roots_of_injective, map_contract, minpoly.isIntegrallyClosed_eq_field_fractions, exists_dvd_map_of_isAlgebraic, coeff_map_eq_comp, mem_lifts, associated_map_map, WeierstrassCurve.baseChange_Ļ, AdjoinRoot.quotEquivQuotMap_apply, map_add, splits_comp_of_splits, Separable.map_irreducible_of_isPurelyInseparable, KummerDedekind.emultiplicity_factors_map_eq_emultiplicity, IsAlgClosed.card_roots_map_eq_natDegree_from_simpleRing, descPochhammer_map, natDegree_map_lt', HurwitzZeta.hurwitzZetaOdd_neg_two_mul_nat, IsCyclotomicExtension.splits_X_pow_sub_one, map_X, aeval_X_left_eq_map, map_ofNat, Irreducible.exists_dvd_monic_irreducible_of_isIntegral, map_injective, one_le_mahlerMeasure_of_ne_zero, degree_map_eq_of_leadingCoeff_ne_zero, hasSum_one_div_nat_pow_mul_cos, IsSplittingField.splits, IsSplittingField.splits', StandardEtalePair.map_g, map_intCast, smul_eq_map, evalā_map, map_id, map_roots_le, mapAlg_eq_map, Splits.roots_map, natDegree_map_eq_of_isUnit_leadingCoeff, Function.Injective.monic_map_iff, IsPrimitive.Int.irreducible_iff_irreducible_map_cast, eval_intCast_map, WeierstrassCurve.baseChange_Ī¦, IsSepClosed.splits_domain, IsPrimitiveRoot.minpoly_dvd_mod_p, SplittingField.splits, splits_id_iff_splits, UniversalFactorizationRing.monicDegreeEq_coe, StandardEtalePair.map_f, LinearMap.polyCharpolyAux_map_eq_charpoly, ascPochhammer_map, Cubic.splits_iff_roots_eq_three, WeierstrassCurve.Affine.CoordinateRing.map_mk, IsPrimitiveRoot.separable_minpoly_mod, map_mapRingHom_evalEval, FiniteField.splits_X_pow_nat_card_sub_X, ConjRootClass.splits_minpoly, WeierstrassCurve.map_Ī¦, WeierstrassCurve.map_preĪØ', AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, AlgebraicClosure.Monics.splits_finsetProd, HurwitzZeta.hurwitzZetaEven_one_sub_two_mul_nat, HurwitzZeta.sinZeta_two_mul_nat_add_one', eval_one_map, sylvester_map_map, WeierstrassCurve.Affine.baseChange_addPolynomial, AdjoinRoot.quotEquivQuotMap_apply_mk, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply, map_roots_le_of_injective, Bivariate.swap_map_C, IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree, minpoly.dvd_map_of_isScalarTower, degree_map_eq_of_injective, map_prod, WeierstrassCurve.baseChange_ĪØ, filter_roots_map_range_eq_map_roots, WeierstrassCurve.Affine.map_polynomial, isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow, derivativeFinsupp_map, monomial_mem_lifts_and_degree_eq, gcd_map, Separable.map, map_restriction, WeierstrassCurve.Affine.baseChange_polynomialX, LinearMap.polyCharpolyAux_baseChange, leadingCoeff_map_of_injective, AdjoinRoot.Polynomial.quotQuotEquivComm_mk, PerfectField.splits_of_natSepDegree_eq_one, eval_map_apply, contentIdeal_map_eq_map_contentIdeal, MonicDegreeEq.map_coe, minpoly.map_algebraMap, card_roots_map_le_natDegree, WeierstrassCurve.map_ĪØSq, IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast, coe_mapRingHom, LinearMap.polyCharpoly_eq_of_basis, PolyEquivTensor.toFunAlgHom_apply_tmul_eq_smul, Algebra.IsAlgebraic.isNormalClosure_iff, LinearMap.polyCharpolyAux_map_aeval, MulSemiringActionHom.coe_polynomial, Monic.natDegree_map, RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_apply, Gal.splits_in_splittingField_of_comp, minpoly.ofSubring, normal_iff, map_expand_pow_char, Ideal.polynomialQuotientEquivQuotientPolynomial_symm_mk, WeierstrassCurve.Affine.baseChange_polynomial, eval_zero_map, nextCoeff_map_eq, roots_map_of_map_ne_zero_of_card_eq_natDegree, IsPrimitiveRoot.squarefree_minpoly_mod, AlgebraicClosure.Monics.map_eq_prod, minpoly.dvd_map_of_isScalarTower', IsAlgClosed.card_roots_map_eq_natDegree_of_injective, map_zero, FiniteField.splits_X_pow_card_sub_X, WeierstrassCurve.baseChange_Ļ, Chebyshev.map_C, polynomial_expand_eq, ascPochhammer_eval_comp, resultant_map_map, HurwitzZeta.sinZeta_two_mul_nat_add_one, map_smul, IsSepClosed.splits_codomain, map_cyclotomic_int, natDegree_map_of_leadingCoeff_ne_zero, nextCoeff_map_of_leadingCoeff_ne_zero, IntermediateField.isSplittingField_iff, Chebyshev.map_T, Splits.map_roots, aeval_sumIDeriv_eq_eval, Monic.roots_map_of_card_eq_natDegree, WeierstrassCurve.map_preĪØ, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk, SplittingFieldAux.splits, mem_roots_map, LinearMap.polyCharpoly_map_eq_charpoly, WeierstrassCurve.map_ĪØā, PolyEquivTensor.toFunBilinear_apply_eq_smul, support_map_subset, splits_of_splits_id, hasSum_one_div_nat_pow_mul_sin, IsAlgClosed.card_roots_map_eq_natDegree_of_leadingCoeff_ne_zero, natDegree_map_le, degree_map_eq_iff, mem_lifts_and_degree_eq, AdjoinRoot.Polynomial.quotQuotEquivComm_symm_mk_mk, Bivariate.swap_C, map_sub, Matrix.charmatrix_map, IsPurelyInseparable.minpoly_eq_X_sub_C_pow, map_sum, WeierstrassCurve.Affine.map_polynomialX, minpolyDiv_spec, leadingCoeff_map_of_leadingCoeff_ne_zero, WeierstrassCurve.map_preĪØā, eval_map_algebraMap, map_cyclotomic, AdjoinRoot.quotEquivQuotMap_symm_apply, IsWeaklyEisensteinAt.map, isIntegrallyClosed_iff', Ring.DirectLimit.Polynomial.exists_of, Normal.out, expand_char, Matrix.charpoly.univ_map_evalāHom, isRoot_map_iff, KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map, card_roots_le_map_of_injective, MvPolynomial.finSuccEquiv_rename_finSuccEquiv, map_neg, map_eq_zero_iff, IntermediateField.adjoin_minpoly_coeff_of_exists_primitive_element, map_dvd_map, MvPolynomial.universalFactorizationMap_freeMonic, IsPrimitiveRoot.pow_isRoot_minpoly, evalEval_map_C, natDegree_map_eq_of_injective, map_frobenius_expand, leadingCoeff_map, degree_map, map_eq_zero, isCoprime_map, X_sub_C_mul_removeFactor, map_toSubring, bernsteinPolynomial.map, Cubic.map_roots, Monic.dvd_iff_fraction_map_dvd_fraction_map, derivative_map, map_C, WeierstrassCurve.Affine.map_addPolynomial, leadingCoeff_of_injective, map_comp, Splits.map, cyclotomic_mahlerMeasure_eq_one, lifts_iff_set_range, map_map, minpoly.iterateFrobenius_of_isSeparable, Monic.exists_splits_map, map_monic_eq_zero_iff, map_multiset_prod, map_mapRingHom_eval_map, MvPolynomial.coeff_eval_eq_eval_coeff, lifts_and_natDegree_eq_and_monic, Ideal.polynomialQuotientEquivQuotientPolynomial_map_mk, WeierstrassCurve.Affine.baseChange_polynomialY, map_surjective_iff, Monic.map, MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix, mul_star_dvd_of_aeval_eq_zero_im_ne_zero, Chebyshev.map_U, iterate_derivative_map, Cubic.map_toPoly, WeierstrassCurve.map_Ļ, Monic.irreducible_iff_irreducible_map_fraction_map, Splits.roots_map_of_ne_zero, map_natCast, MvPolynomial.optionEquivLeft_elim_eval, IsPrimitive.isUnit_iff_isUnit_map, degree_map_lt, mapEquiv_apply, map_mapRingHom_eval_map_eval, finite_mahlerMeasure_le, WeierstrassCurve.Affine.CoordinateRing.map_smul, aroots_def, map_map_freeMonic, matPolyEquiv_smul_one, evalā_eq_eval_map, PowerSeries.trunc_map, Gal.splits_ā_ā, map_dvd_map', map_evalRingHom_eval, map_divByMonic, nextCoeff_map_eq_of_isUnit_leadingCoeff, IsGalois.splits, IsAlgClosed.splits_domain, Monic.degree_map, polynomial_map_coe, support_map_of_injective, isSplittingField_iff_intermediateField, map_aeval_eq_aeval_map, residueFieldMapCAlgEquiv_algebraMap, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of, natDegree_map_lt, WeierstrassCurve.baseChange_ĪØā, minpoly.map_eq_of_equiv_equiv, IsSplittingField.map, map_scaleRoots, LinearMap.charpoly_baseChange, separable_map, polyEquivTensor_symm_apply_tmul_eq_smul, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, roots_map, evalā_evalāRingHom_apply, IsPrimitive.dvd_iff_fraction_map_dvd_fraction_map, Chebyshev.map_S, coe_mapAlgHom, IsRoot.map, card_mahlerMeasure_le_prod, map_iterateFrobenius_expand, map_normalize, map_mod_divByMonic, AdjoinRoot.isRoot_root, MvPolynomial.universalFactorizationMapPresentation_jacobian, minpoly.isIntegrallyClosed_eq_field_fractions', coe_mapAlgEquiv, MvPolynomial.coe_mapEquivMonic_comp, LinearMap.polyCharpolyAux_map_eq_toMatrix_charpoly, isIntegral_isLocalization_polynomial_quotient, KummerDedekind.quotMapEquivQuotQuotMap_symm_apply, int_cyclotomic_spec
|
mapRingHom š | CompOp | 40 mathmath: WeierstrassCurve.map_Ļā, ker_mapRingHom, Ideal.exists_mem_span_singleton_map_residueField_eq, WeierstrassCurve.map_Ļ, fiberEquivQuotient_tmul, WeierstrassCurve.map_ĪØ, WeierstrassCurve.Affine.map_polynomialY, evalāRingHom_evalāRingHom, Ideal.injective_quotient_le_comap_map, algebraMap_def, WeierstrassCurve.baseChange_Ļā, WeierstrassCurve.Affine.baseChange_negPolynomial, WeierstrassCurve.Affine.map_negPolynomial, WeierstrassCurve.baseChange_Ļ, lifts_iff_ringHom_rangeS, WeierstrassCurve.Affine.CoordinateRing.map_mk, map_mapRingHom_evalEval, mapRingHom_comp_C, eval_C_X_evalā_map_C_X, WeierstrassCurve.baseChange_ĪØ, WeierstrassCurve.Affine.map_polynomial, WeierstrassCurve.Affine.baseChange_polynomialX, coe_mapRingHom, WeierstrassCurve.Affine.baseChange_polynomial, WeierstrassCurve.baseChange_Ļ, mem_map_range, eval_C_X_comp_evalā_map_C_X, WeierstrassCurve.Affine.map_polynomialX, PrimeSpectrum.range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk, mapAlgEquiv_coe_ringHom, mapRingHom_id, mapRingHom_comp, map_mapRingHom_eval_map, WeierstrassCurve.Affine.baseChange_polynomialY, Ideal.quotient_mk_maps_eq, WeierstrassCurve.map_Ļ, mapAlgHom_coe_ringHom, map_mapRingHom_eval_map_eval, mem_map_rangeS, evalā_evalāRingHom_apply
|