| Metric | Count |
|---|
DefinitionscoeToPowerSeries, algHom, ringHom, toPowerSeries, C, X, algebraPolynomial, algebraPolynomial', algebraPowerSeries, coeff, constantCoeff, evalNegHom, map, mapAlgHom, mk, monomial, rescale, toSubring, «term_⟦X⟧» | 19 |
TheoremstoMvPowerSeries_pUnitAlgEquiv, algHom_apply, ringHom_apply, coe_C, coe_X, coe_add, coe_def, coe_eq_one_iff, coe_eq_zero_iff, coe_inj, coe_injective, coe_monomial, coe_mul, coe_neg, coe_one, coe_pow, coe_smul, coe_sub, coe_zero, coeff_coe, constantCoeff_coe, eval₂_C_X_eq_coe, pUnitAlgEquiv_symm_toPowerSeries, polynomial_map_coe, C_eq_algebraMap, C_injective, X_dvd_iff, X_eq, X_mul, X_mul_cancel, X_mul_inj, X_mul_injective, X_ne_zero, X_pow_dvd_iff, X_pow_eq, X_pow_mul, X_pow_mul_cancel, X_pow_mul_inj, X_pow_mul_injective, algebraMap_apply, algebraMap_apply', algebraMap_apply'', algebraMap_eq, coeff_C, coeff_C_mul, coeff_C_mul_X_pow, coeff_X, coeff_X_pow, coeff_X_pow_mul, coeff_X_pow_mul', coeff_X_pow_self, coeff_comp_monomial, coeff_def, coeff_map, coeff_mk, coeff_monomial, coeff_monomial_same, coeff_mul, coeff_mul_C, coeff_mul_X_pow, coeff_mul_X_pow', coeff_ne_zero_C, coeff_one, coeff_one_X, coeff_one_mul, coeff_one_pow, coeff_pow, coeff_prod, coeff_rescale, coeff_smul, coeff_succ_C, coeff_succ_X_mul, coeff_succ_mul_X, coeff_toSubring, coeff_zero_C, coeff_zero_X, coeff_zero_X_mul, coeff_zero_eq_constantCoeff, coeff_zero_eq_constantCoeff_apply, coeff_zero_mul_X, coeff_zero_one, commute_X, commute_X_pow, constantCoeff_C, constantCoeff_X, constantCoeff_comp_C, constantCoeff_mk, constantCoeff_one, constantCoeff_smul, constantCoeff_surj, constantCoeff_toSubring, constantCoeff_zero, eq_X_mul_shift_add_const, eq_shift_mul_X_add_const, evalNegHom_X, ext, ext_iff, forall_coeff_eq_zero, instNontrivialSubalgebra, instSubsingleton, isUnit_constantCoeff, mapAlgHom_apply, map_C, map_X, map_comp, map_eq_zero, map_id, map_injective, map_surjective, map_toSubring, monomial_eq_mk, monomial_mul_monomial, monomial_pow, monomial_zero_eq_C, monomial_zero_eq_C_apply, mul_X_cancel, mul_X_inj, mul_X_injective, mul_X_pow_cancel, mul_X_pow_inj, mul_X_pow_injective, not_isField, prod_monomial, rescale_X, rescale_algebraMap_map, rescale_map, rescale_mk, rescale_mul, rescale_neg_one_X, rescale_one, rescale_rescale, rescale_zero, rescale_zero_apply, smul_eq_C_mul, subsingleton_iff | 135 |
| Total | 154 |
| Name | Category | Theorems |
|---|
C 📖 | CompOp | 46 mathmath: Polynomial.eval₂_C_X_eq_coe, coeff_mul_C, heval_C, coeff_ne_zero_C, rescale_X, Polynomial.coe_C, map_constantCoeff_le_self_of_X_mem, trunc_mul_C, rescale_zero_apply, rescale_zero, derivativeFun_C, C_injective, eq_X_mul_shift_add_const, constantCoeff_comp_C, coeff_succ_C, sub_const_eq_X_mul_shift, constantCoeff_C, invUnitsSub_mul_sub, monomial_zero_eq_C, sub_const_eq_shift_mul_X, trunc_C, WithPiTopology.continuous_C, coe_C, gaussNorm_C, subst_C, expand_C, C_eq_algebraMap, eval₂_C, eq_shift_mul_X_add_const, coeff_zero_C, coeff_C, monomial_eq_C_mul_X_pow, algebraMap_eq, map_C, C_inv, algebraMap_apply, coeff_C_mul, derivative_C, invUnitsSub_mul_X, coeff_C_mul_X_pow, HahnSeries.ofPowerSeries_C, smul_eq_C_mul, monomial_zero_eq_C_apply, IsRestricted.C, trunc_C_mul, eq_span_insert_X_of_X_mem_of_span_eq
|
X 📖 | CompOp | 117 mathmath: Polynomial.eval₂_C_X_eq_coe, rescale_eq_subst, coeff_X_mul_largeSchroderSeries, expand_apply, trunc_X_pow_self_mul, invOneSubPow_inv_eq_one_sub_pow, coeff_succ_mul_X, X_prime, maximalIdeal_eq_span_X, HahnSeries.ofPowerSeries_X_pow, rescale_X, Nat.Partition.tendsto_order_genFun_term_atTop_nhds_top, Polynomial.bernoulli_generating_function, eval₂_X, constantCoeff_X, eq_shift_mul_X_pow_add_trunc, bernoulliPowerSeries_mul_exp_sub_one, IsWeierstrassFactorization.isWeierstrassDivision, normUnit_X, coeff_X_mul_largeSchroderSeriesSeries_sq, mk_add_choose_mul_one_sub_pow_eq_one, HasSubst.X', commute_X_pow, substAlgHom_X, Nat.Partition.hasProd_powerSeriesMk_card_countRestricted, aeval_unique, HasSubst.X_pow, largeSchroderSeries_eq_one_add_X_mul_largeSchroderSeries_add_X_mul_largeSchroderSeries_sq, bernoulli'PowerSeries_mul_exp_sub_one, mul_X_injective, trunc_X_of, normalized_count_X_eq_of_coe, HasSubst.smul_X', Nat.Partition.summable_genFun_term, eq_X_mul_shift_add_const, evalNegHom_X, X_pow_mul, Polynomial.coe_X, Nat.Partition.powerSeriesMk_card_restricted_eq_tprod, X_inv, sub_const_eq_X_mul_shift, LaurentSeries.of_powerSeries_localization, invUnitsSub_mul_sub, X_irreducible, eq_X_pow_mul_shift_add_trunc, HahnSeries.ofPowerSeries_X, X_mul_inj, one_sub_pow_add_mul_invOneSubPow_val_eq_one_sub_pow, LaurentSeries.coe_X_compare, sub_const_eq_shift_mul_X, one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val, map_X, Nat.Partition.hasProd_powerSeriesMk_card_restricted, X_eq, map_algebraMap_eq_subst_X, X_mul, X_pow_mul_injective, coeff_X, Nat.Partition.powerSeriesMk_card_countRestricted_eq_tprod, heval_X, eq_shift_mul_X_add_const, coeff_mul_X_pow', coeff_subst_X_pow, coe_X, X_pow_eq, monomial_eq_C_mul_X_pow, mul_X_pow_injective, Nat.Partition.summable_genFun_term', Nat.Partition.multipliable_powerSeriesMk_card_restricted, X_pow_order_dvd, coeff_X_pow_self, invOneSubPow_eq_inv_one_sub_pow, intValuation_X, subst_X, rescale_neg_one_X, catalanSeries_sq_mul_X_add_one, coeff_X_pow, trunc_one_X, X_pow_order_mul_divXPowOrder, coeff_succ_X_mul, span_X_isPrime, order_X, Nat.Partition.hasProd_genFun, X_pow_dvd_iff, X_pow_mul_inj, expand_X, coeff_zero_X_mul, X_dvd_iff, invUnitsSub_mul_X, coeff_C_mul_X_pow, order_eq_emultiplicity_X, coeff_X_pow_mul', binomialSeries_nat, coeff_mul_X_pow, Nat.Partition.multipliable_powerSeriesMk_card_countRestricted, WithPiTopology.multipliable_one_sub_X_pow, order_X_pow, LaurentSeries.X_order_mul_powerSeriesPart, mul_X_pow_inj, mk_one_mul_one_sub_eq_one, constantCoeff_subst_X_pow, HasEval.X, mul_X_inj, Nat.Partition.multipliable_genFun, divXPowOrder_X, trunc_X, X_mul_injective, derivative_X, coeff_X_pow_mul, coeff_zero_mul_X, LaurentSeries.valuation_X_pow, Nat.Partition.genFun_eq_tprod, commute_X, X_eq_normalizeX, coeff_one_X, eq_span_insert_X_of_X_mem_of_span_eq, coeff_zero_X
|
algebraPolynomial 📖 | CompOp | 15 mathmath: RatFunc.instFaithfulSMulPolynomialLaurentSeries, RatFunc.coe_X, RatFunc.coe_coe, LaurentSeries.inducing_coe, LaurentSeries.continuous_coe, LaurentSeries.exists_ratFunc_val_lt, RatFunc.valuation_eq_LaurentSeries_valuation, RatFunc.algebraMap_apply_div, LaurentSeries.continuous_coe', LaurentSeries.LaurentSeries_coe, Polynomial.algebraMap_hahnSeries_apply, Polynomial.algebraMap_hahnSeries_injective, LaurentSeries.valuation_coe_ratFunc, LaurentSeries.coe_range_dense, algebraMap_apply'
|
algebraPolynomial' 📖 | CompOp | — |
algebraPowerSeries 📖 | CompOp | 1 mathmath: algebraMap_apply''
|
coeff 📖 | CompOp | 142 mathmath: coeff_mul_eq_coeff_trunc_mul_trunc₂, coeff_toSubring, CuspFormClass.qExpansion_isBigO, WithPiTopology.hasSum_iff_hasSum_coeff, hasSum_aeval, coeff_mul_one_sub_of_lt_order, coeff_mul_of_lt_order, coeff_of_lt_order_toNat, constantCoeff_subst, WithPiTopology.continuous_coeff, ModularFormClass.qExpansionFormalMultilinearSeries_apply_norm, coeff_mul_C, coeff_rescale, coeff_expand_mul, catalanSeries_coeff, coeff_X_mul_largeSchroderSeries, coeff_trunc, coeff_of_lt_order, coeff_succ_mul_X, coeff_mul_mem_ideal_of_coeff_right_mem_ideal', coeff_ne_zero_C, aeval_eq_sum, binomialSeries_coeff, coeff_subst, coeff_coe, eq_shift_mul_X_pow_add_trunc, IsWeierstrassDivisorAt.coeff_seq_succ_sub_seq_mem, coeff_inv_aux, WithPiTopology.tendsto_iff_coeff_tendsto, WithPiTopology.uniformContinuous_coeff, coeff_zero_one, coeff_X_mul_largeSchroderSeriesSeries_sq, coeff_invOfUnit, hasSum_of_monomials_self, coeff_derivativeFun, eval₂_eq_tsum, eq_X_mul_shift_add_const, LaurentSeries.powerSeriesPart_coeff, coeff_invUnitsSub, coeff_succ_C, IsRestricted.isRestricted_iff, coeff_mul_mem_ideal_of_coeff_right_mem_ideal, coeff_mk, sub_const_eq_X_mul_shift, coeff_largeSchroderSeries, HahnSeries.ofPowerSeries_apply_coeff, eq_X_pow_mul_shift_add_trunc, ModularFormClass.qExpansion_coeff, coeff_exp, trunc_one_left, sub_const_eq_shift_mul_X, LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero, IsWeierstrassDivisorAt.isUnit_shift, Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval, constantCoeff_divXPowOrder, HahnSeries.toPowerSeriesAlg_symm_apply_coeff, ModularFormClass.qExpansion_coeff_zero, coeff_comp_monomial, coeff_mul, coeff_def, HahnSeries.coeff_toPowerSeries, IsWeierstrassDivisorAt.coeff_seq_mem, coeff_smul, coeff_monomial_same, trunc_apply, coeff_mul_mem_ideal_of_coeff_left_mem_ideal', coeff_monomial, coeff_X, HahnSeries.coeff_toPowerSeries_symm, IsWeierstrassDivisorAt.coeff_div, EisensteinSeries.E_qExpansion_coeff, as_tsum, coeff_zero_eq_constantCoeff_apply, HahnSeries.ofPowerSeriesAlg_apply_coeff, ModularFormClass.hasSum_qExpansion_of_abs_lt, coeff_map, coeff_one, eq_shift_mul_X_add_const, coeff_prod, coeff_mul_X_pow', coeff_zero_C, forall_coeff_eq_zero, coeff_C, coeff_inv, ModularFormClass.qExpansion_coeff_eq_circleIntegral, coeff_expand_of_not_dvd, coeff_subst_X_pow, coeff_zero_eq_constantCoeff, LaurentSeries.coeff_zero_of_lt_intValuation, le_gaussNorm, coeff_divXPowOrder, HahnSeries.SummableFamily.powerSeriesFamily_of_orderTop_pos, ext_iff, coeff_X_pow_self, trunc_succ, ModularFormClass.qExpansion_isBigO, coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal, coeff_mul_eq_coeff_trunc_mul_trunc, qExpansion_mul_coeff_zero, coeff_derivative, coeff_subst_finite, coeff_X_pow, ModularFormClass.hasSum_qExpansion_of_norm_lt, qExpansion_coeff_unique, coeff_subst', coeff_expand, eval₂_trunc_eq_sum_range, coeff_succ_X_mul, coeff_C_mul, X_pow_dvd_iff, coeff_mul_mem_ideal_of_coeff_left_mem_ideal, order_eq, coeff_zero_X_mul, EisensteinSeries.E_qExpansion_coeff_zero, coeff_C_mul_X_pow, coeff_X_pow_mul', coeff_pow, coeff_one_pow, coeff_mul_X_pow, ModularFormClass.qExpansionFormalMultilinearSeries_coeff, IsWeierstrassDivisorAt.seq_one, Nat.Partition.coeff_genFun, coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal', coeff_subst_finite', coeff_coe_trunc_of_lt, coeff_mul_prod_one_sub_of_lt_order, HahnSeries.toPowerSeries_symm_apply_coeff, LaurentSeries.coeff_coe_powerSeries, ModularFormClass.hasSum_qExpansion, qExpansion_coeff_isBigO_of_norm_isBigO, ModularFormClass.qExpansion_coeff_eq_intervalIntegral, coeff_one_mul, Polynomial.coeff_coe, IsWeierstrassDivisorAt.coeff_div_sub_seq_mem, coeff_X_pow_mul, coeff_zero_mul_X, WithPiTopology.summable_iff_summable_coeff, hasSum_eval₂, coeff_one_X, order_eq_nat, coeff_zero_X, IsWeierstrassDivisionAt.coeff_f_sub_r_mem
|
constantCoeff 📖 | CompOp | 50 mathmath: constantCoeff_expand, spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_X_mem, spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_isPrime, catalanSeries_constantCoeff, constantCoeff_X, isUnit_iff_constantCoeff, WithPiTopology.continuous_constantCoeff, map_constantCoeff_le_self_of_X_mem, constantCoeff_invUnitsSub, rescale_zero_apply, rescale_zero, constantCoeff_surj, constantCoeff_one, constantCoeff_invOfUnit, Polynomial.constantCoeff_coe, eq_X_mul_shift_add_const, constantCoeff_comp_C, one_le_order_iff_constCoeff_eq_zero, HahnSeries.SummableFamily.powerSeriesFamily_hsum_zero, sub_const_eq_X_mul_shift, constantCoeff_C, constantCoeff_inv, WithPiTopology.isTopologicallyNilpotent_iff_constantCoeff_isNilpotent, spanFinrank_eq_spanFinrank_map_constantCoeff_of_X_notMem_of_fg_of_isPrime, sub_const_eq_shift_mul_X, constantCoeff_divXPowOrder, inv_eq_zero, constantCoeff_largeSchroderSeries, invOfUnit_eq, constantCoeff_divXPowOrder_eq_zero_iff, constantCoeff_zero, fg_iff_of_isPrime, coeff_zero_eq_constantCoeff_apply, constantCoeff_smul, constantCoeff_mk, eq_shift_mul_X_add_const, coeff_inv, coeff_zero_eq_constantCoeff, ker_coeff_eq_max_ideal, constantCoeff_exp, constantCoeff_toSubring, inv_eq_inv_aux, coeff_heval_zero, order_ne_zero_iff_constCoeff_eq_zero, X_dvd_iff, binomialSeries_constantCoeff, coeff_one_pow, coeff_one_mul, constantCoeff_subst_X_pow, isUnit_constantCoeff
|
evalNegHom 📖 | CompOp | 2 mathmath: exp_mul_exp_neg_eq_one, evalNegHom_X
|
map 📖 | CompOp | 39 mathmath: algebraMap_apply'', degree_weierstrassMod_lt, mapAlgHom_apply, Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_map, map_cos, IsWeierstrassFactorization.isWeierstrassDivision, IsWeierstrassDivisionAt.degree_lt, IsWeierstrassFactorizationAt.natDegree_eq_toNat_order_map_of_ne_top, le_order_map, map_sin, rescale_algebraMap_map, IsWeierstrassFactorization.natDegree_eq_toNat_order_map, map_eq_zero, rescale_map, IsWeierstrassDivisorAt.isUnit_shift, map_X, map_comp, map_subst, map_algebraMap_eq_subst_X, map_surjective, map_invUnitsSub, Polynomial.coeToPowerSeries.algHom_apply, coeff_map, map_expand, map_C, IsWeierstrassDivision.isWeierstrassFactorization, IsWeierstrassFactorization.degree_eq_coe_lift_order_map, IsWeierstrassFactorizationAt.degree_eq_coe_lift_order_map_of_ne_top, isWeierstrassDivisionAt_iff, map_exp, algebraMap_apply', IsWeierstrassDivisorAt.seq_one, map_id, trunc_map, Polynomial.polynomial_map_coe, map_toSubring, map.isLocalHom, map_injective, Polynomial.IsDistinguishedAt.coe_natDegree_eq_order_map
|
mapAlgHom 📖 | CompOp | 1 mathmath: mapAlgHom_apply
|
mk 📖 | CompOp | — |
monomial 📖 | CompOp | 21 mathmath: gaussNorm_monomial, Polynomial.coe_monomial, hasSum_of_monomials_self, order_monomial, monomial_mul_monomial, prod_monomial, monomial_zero_eq_C, monomial_pow, HasSubst.monomial', monomial_eq_mk, X_eq, coeff_comp_monomial, coeff_monomial_same, coeff_monomial, as_tsum, X_pow_eq, monomial_eq_C_mul_X_pow, expand_monomial, IsRestricted.monomial, monomial_zero_eq_C_apply, order_monomial_of_ne_zero
|
rescale 📖 | CompOp | 21 mathmath: rescale_eq_subst, coeff_rescale, MvPowerSeries.rescaleUnit, rescale_X, subst_rescale_of_degree_eq_one, Polynomial.bernoulli_generating_function, rescale_rescale, rescale_zero_apply, rescale_zero, rescale_mk, rescale_algebraMap_map, exp_mul_exp_eq_exp_add, rescale_map, rescale_injective, exp_pow_eq_rescale_exp, rescale_neg_one_X, coe_rescaleAlgHom, rescale_eq, rescale_one, rescale_neg_one_invOneSubPow, rescale_mul
|
toSubring 📖 | CompOp | 4 mathmath: coeff_toSubring, order_toSubring, constantCoeff_toSubring, map_toSubring
|
«term_⟦X⟧» 📖 | CompOp | — |