| Name | Category | Theorems |
|---|
C 📖 | CompOp | 45 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, 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 | 113 mathmath: Polynomial.eval₂_C_X_eq_coe, 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', 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, 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, coeff_zero_X
|
algebraPolynomial 📖 | CompOp | 14 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.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 | 131 mathmath: coeff_mul_eq_coeff_trunc_mul_trunc₂, 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_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_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_monomial, coeff_X, HahnSeries.coeff_toPowerSeries_symm, IsWeierstrassDivisorAt.coeff_div, 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_zero_eq_constantCoeff, LaurentSeries.coeff_zero_of_lt_intValuation, coeff_divXPowOrder, HahnSeries.SummableFamily.powerSeriesFamily_of_orderTop_pos, ext_iff, coeff_X_pow_self, trunc_succ, ModularFormClass.qExpansion_isBigO, 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, order_eq, coeff_zero_X_mul, 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_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 | 49 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, isUnit_constantCoeff
|
evalNegHom 📖 | CompOp | 2 mathmath: exp_mul_exp_neg_eq_one, evalNegHom_X
|
instAddCommGroup 📖 | CompOp | 14 mathmath: IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply, derivative_inv', IsWeierstrassDivisorAt.mod'_mk_eq_mod, evalNegHom_X, IsRestricted.neg, derivative_invOf, coe_neg, Polynomial.IsDistinguishedAt.algEquivQuotient_symm_apply, Polynomial.coe_neg, qExpansion_neg, rescale_neg_one_X, order_neg, IsWeierstrassDivisorAt.mk_mod'_eq_self, derivative_inv
|
instAddCommMonoid 📖 | CompOp | 203 mathmath: coeff_mul_eq_coeff_trunc_mul_trunc₂, CuspFormClass.qExpansion_isBigO, WithPiTopology.hasSum_iff_hasSum_coeff, hasSum_aeval, coeff_mul_one_sub_of_lt_order, coeff_mul_of_lt_order, IsRestricted.smul, 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, trunc_mul_trunc, trunc_X_pow_self_mul, derivative_exp, coeff_of_lt_order, coeff_succ_mul_X, gaussNorm_monomial, coeff_ne_zero_C, derivative_inv', Polynomial.coe_monomial, aeval_eq_sum, binomialSeries_coeff, coeff_subst, le_order_smul, coeff_coe, eq_shift_mul_X_pow_add_trunc, IsWeierstrassDivisorAt.coeff_seq_succ_sub_seq_mem, coeff_inv_aux, degree_trunc_lt, WithPiTopology.tendsto_iff_coeff_tendsto, coe_smul, WithPiTopology.uniformContinuous_coeff, coeff_zero_one, coeff_X_mul_largeSchroderSeriesSeries_sq, trunc_trunc_mul_trunc, coeff_invOfUnit, trunc_mul_C, hasSum_of_monomials_self, Nat.Partition.hasProd_powerSeriesMk_card_countRestricted, coeff_derivativeFun, eval₂_eq_tsum, trunc_X_of, instIsScalarTower, WithPiTopology.summable_prod_of_tendsto_order_atTop_nhds_top, order_monomial, monomial_mul_monomial, Nat.Partition.summable_genFun_term, eq_X_mul_shift_add_const, LaurentSeries.powerSeriesPart_coeff, coeff_invUnitsSub, prod_monomial, coeff_succ_C, trunc_trunc_mul, Nat.Partition.powerSeriesMk_card_restricted_eq_tprod, IsRestricted.isRestricted_iff, exp_pow_sum, coeff_mk, Polynomial.coe_smul, sub_const_eq_X_mul_shift, coeff_largeSchroderSeries, HahnSeries.ofPowerSeries_apply_coeff, monomial_zero_eq_C, monomial_pow, eq_X_pow_mul_shift_add_trunc, trunc_trunc_of_le, ModularFormClass.qExpansion_coeff, coeff_exp, trunc_one_left, sub_const_eq_shift_mul_X, LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero, WithPiTopology.one_sub_mul_tsum_pow_of_constantCoeff_eq_zero, derivative_invOf, HasSubst.monomial', IsWeierstrassDivisorAt.isUnit_shift, Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval, constantCoeff_divXPowOrder, monomial_eq_mk, HahnSeries.toPowerSeriesAlg_symm_apply_coeff, trunc_C, Nat.Partition.hasProd_powerSeriesMk_card_restricted, ModularFormClass.qExpansion_coeff_zero, X_eq, coeff_comp_monomial, trunc_trunc_pow, coeff_mul, HahnSeries.coeff_toPowerSeries, IsWeierstrassDivisorAt.coeff_seq_mem, coeff_smul, coeff_monomial_same, trunc_apply, coeff_monomial, coeff_X, HahnSeries.coeff_toPowerSeries_symm, IsWeierstrassDivisorAt.coeff_div, as_tsum, Nat.Partition.powerSeriesMk_card_countRestricted_eq_tprod, derivative_coe, coeff_zero_eq_constantCoeff_apply, HahnSeries.ofPowerSeriesAlg_apply_coeff, ModularFormClass.hasSum_qExpansion_of_abs_lt, coeff_map, constantCoeff_smul, 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, WithPiTopology.tsum_pow_mul_one_sub_of_constantCoeff_eq_zero, coeff_expand_of_not_dvd, coeff_zero_eq_constantCoeff, LaurentSeries.coeff_zero_of_lt_intValuation, X_pow_eq, monomial_eq_C_mul_X_pow, Nat.Partition.summable_genFun_term', Nat.Partition.multipliable_powerSeriesMk_card_restricted, coeff_divXPowOrder, trunc_one, HahnSeries.SummableFamily.powerSeriesFamily_of_orderTop_pos, ext_iff, coeff_X_pow_self, trunc_succ, ModularFormClass.qExpansion_isBigO, coeff_mul_eq_coeff_trunc_mul_trunc, qExpansion_mul_coeff_zero, trunc_coe_eq_self, coeff_derivative, coeff_subst_finite, coeff_X_pow, ModularFormClass.hasSum_qExpansion_of_norm_lt, expand_monomial, qExpansion_coeff_unique, coeff_subst', derivative_subst, IsRestricted.monomial, coeff_expand, eval₂_trunc_eq_sum_range, trunc_one_X, coeff_succ_X_mul, trunc_trunc, Nat.Partition.hasProd_genFun, coeff_C_mul, X_pow_dvd_iff, derivative_C, order_eq, coeff_zero_X_mul, WithPiTopology.tendsto_trunc_atTop, coeff_C_mul_X_pow, coeff_X_pow_mul', coeff_pow, coeff_one_pow, coeff_mul_X_pow, smul_eq_C_mul, ModularFormClass.qExpansionFormalMultilinearSeries_coeff, trunc_sub, IsWeierstrassDivisorAt.seq_one, Nat.Partition.coeff_genFun, Nat.Partition.multipliable_powerSeriesMk_card_countRestricted, trunc_derivativeFun, WithPiTopology.summable_of_tendsto_order_atTop_nhds_top, coeff_subst_finite', trunc_map, coeff_coe_trunc_of_lt, trunc_zero', coeff_mul_prod_one_sub_of_lt_order, HahnSeries.toPowerSeries_symm_apply_coeff, trunc_derivative, LaurentSeries.coeff_coe_powerSeries, ModularFormClass.hasSum_qExpansion, qExpansion_coeff_isBigO_of_norm_isBigO, ModularFormClass.qExpansion_coeff_eq_intervalIntegral, coeff_one_mul, monomial_zero_eq_C_apply, Nat.Partition.multipliable_genFun, Polynomial.coeff_coe, derivative_inv, natDegree_trunc_lt, trunc_X, derivative_X, WithPiTopology.summable_pow_of_constantCoeff_eq_zero, IsWeierstrassDivisorAt.coeff_div_sub_seq_mem, coeff_X_pow_mul, coeff_zero_mul_X, Nat.Partition.genFun_eq_tprod, order_monomial_of_ne_zero, trunc_C_mul, WithPiTopology.summable_iff_summable_coeff, hasSum_eval₂, coeff_one_X, derivative_pow, order_eq_nat, coeff_zero_X, IsWeierstrassDivisionAt.coeff_f_sub_r_mem, trunc_derivative'
|
instAddGroup 📖 | CompOp | 28 mathmath: coeff_mul_one_sub_of_lt_order, invOneSubPow_inv_eq_one_sub_pow, Polynomial.bernoulli_generating_function, bernoulliPowerSeries_mul_exp_sub_one, IsWeierstrassDivisorAt.coeff_seq_succ_sub_seq_mem, mk_add_choose_mul_one_sub_pow_eq_one, coe_sub, bernoulli'PowerSeries_mul_exp_sub_one, LaurentSeries.exists_Polynomial_intValuation_lt, sub_const_eq_X_mul_shift, invUnitsSub_mul_sub, one_sub_pow_add_mul_invOneSubPow_val_eq_one_sub_pow, sub_const_eq_shift_mul_X, qExpansion_sub, WithPiTopology.one_sub_mul_tsum_pow_of_constantCoeff_eq_zero, one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val, IsWeierstrassDivisorAt.coeff_seq_mem, WithPiTopology.instIsUniformAddGroup, Polynomial.coe_sub, WithPiTopology.tsum_pow_mul_one_sub_of_constantCoeff_eq_zero, invOneSubPow_eq_inv_one_sub_pow, invUnitsSub_mul_X, trunc_sub, WithPiTopology.multipliable_one_sub_X_pow, coeff_mul_prod_one_sub_of_lt_order, mk_one_mul_one_sub_eq_one, IsWeierstrassDivisorAt.coeff_div_sub_seq_mem, IsWeierstrassDivisionAt.coeff_f_sub_r_mem
|
instAddMonoid 📖 | CompOp | 8 mathmath: IsRestricted.smul, le_order_smul, coe_smul, instIsScalarTower, Polynomial.coe_smul, coeff_smul, constantCoeff_smul, smul_eq_C_mul
|
instAlgebra 📖 | CompOp | 84 mathmath: IsWeierstrassFactorizationAt.algEquivQuotient_apply, hasSum_aeval, IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply, constantCoeff_expand, heval_C, coeff_expand_mul, expand_apply, derivative_exp, order_expand, mapAlgHom_apply, derivative_inv', Nat.Partition.tendsto_order_genFun_term_atTop_nhds_top, coeff_heval, aeval_eq_sum, support_expand_subset, derivativeFun_smul, support_expand, smul_weierstrassDiv, substAlgHom_X, heval_apply, expand_one_apply, LaurentSeries.algebraMap_apply, substAlgHom_comp_substAlgHom, HasSubst.smul_X', expand_smul, Nat.Partition.summable_genFun_term, IsWeierstrassDivisorAt.mod'_mk_eq_mod, smul_weierstrassMod, instNontrivialSubalgebra, derivative_invOf, HahnSeries.toPowerSeriesAlg_apply, HahnSeries.toPowerSeriesAlg_symm_apply_coeff, expand_C, C_eq_algebraMap, expand_mul, IsWeierstrassDivisorAt.mod_smul, expand_mul_eq_comp, Polynomial.coeToPowerSeries.algHom_apply, derivative_coe, HahnSeries.ofPowerSeriesAlg_apply_coeff, Polynomial.IsDistinguishedAt.algEquivQuotient_symm_apply, heval_X, comp_aeval, map_expand, coeff_expand_of_not_dvd, Nat.Partition.summable_genFun_term', HasSubst.comp, algebraMap_eq, continuous_aeval, heval_unit, coeff_derivative, expand_monomial, derivative_subst, coeff_expand, algebraMap_apply, coe_aeval, expand_one, IsWeierstrassDivisorAt.mk_mod'_eq_self, aeval_coe, Nat.Partition.hasProd_genFun, coeff_heval_zero, IsWeierstrassFactorizationAt.smul, substAlgHom_coe, derivative_C, IsWeierstrassDivisorAt.div_smul, expand_X, subst_smul, IsWeierstrassDivisionAt.smul, substAlgHom_comp_substAlgHom_apply, weierstrassUnit_smul, heval_mul, smul_inv, qExpansion_smul, trunc_derivative, Polynomial.IsDistinguishedAt.algEquivQuotient_apply, Nat.Partition.multipliable_genFun, HahnSeries.SummableFamily.powerSeriesFamily_smul, derivative_inv, coe_substAlgHom, derivative_X, weierstrassDistinguished_smul, Nat.Partition.genFun_eq_tprod, derivative_pow, trunc_derivative'
|
instCommRing 📖 | CompOp | 32 mathmath: IsWeierstrassFactorizationAt.algEquivQuotient_apply, HahnSeries.SummableFamily.powerSeriesFamily_add, IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply, eq_mul_weierstrassDiv_add_weierstrassMod, intValuation_eq_of_coe, IsWeierstrassDivisionAt.eq_mul_add, aeval_unique, IsWeierstrassDivisorAt.mod'_mk_eq_mod, LaurentSeries.exists_Polynomial_intValuation_lt, RatFunc.valuation_eq_LaurentSeries_valuation, IsWeierstrassDivisorAt.mod_add, hasUnitMulPowIrreducibleFactorization, qExpansion_add, instIsDiscreteValuationRing, subst_add, LaurentSeries.powerSeriesRingEquiv_coe_apply, LaurentSeries.powerSeriesEquivSubring_apply, Polynomial.IsDistinguishedAt.algEquivQuotient_symm_apply, IsWeierstrassDivisionAt.add, add_weierstrassMod, IsWeierstrassDivisorAt.div_add, LaurentSeries.powerSeriesEquivSubring_coe_apply, invOneSubPow_eq_inv_one_sub_pow, intValuation_X, isWeierstrassDivisionAt_iff, LaurentSeries.valuation_def, IsWeierstrassDivisorAt.mk_mod'_eq_self, WithPiTopology.multipliable_one_sub_X_pow, coeff_mul_prod_one_sub_of_lt_order, Polynomial.IsDistinguishedAt.algEquivQuotient_apply, add_weierstrassDiv, HasEval.X
|
instCommSemiring 📖 | CompOp | 42 mathmath: derivative_exp, algebraMap_apply'', instUniqueFactorizationMonoidOfIsPrincipalIdealRingOfIsDomain, X_prime, maximalIdeal_eq_span_X, divXPowOrder_prod, derivative_inv', LaurentSeries.coe_algebraMap, ringKrullDim_succ_le_ringKrullDim_powerseries, normUnit_X, Nat.Partition.hasProd_powerSeriesMk_card_countRestricted, WithPiTopology.summable_prod_of_tendsto_order_atTop_nhds_top, normalized_count_X_eq_of_coe, prod_monomial, instUniqueFactorizationMonoid, Nat.Partition.powerSeriesMk_card_restricted_eq_tprod, LaurentSeries.of_powerSeries_localization, derivative_invOf, Nat.Partition.hasProd_powerSeriesMk_card_restricted, Nat.Partition.powerSeriesMk_card_countRestricted_eq_tprod, derivative_coe, coeff_prod, order_prod, Nat.Partition.multipliable_powerSeriesMk_card_restricted, ker_coeff_eq_max_ideal, coeff_derivative, derivative_subst, Nat.Partition.hasProd_genFun, WithPiTopology.multipliable_one_add_of_tendsto_order_atTop_nhds_top, derivative_C, LaurentSeries.instIsFractionRingPowerSeries, Nat.Partition.multipliable_powerSeriesMk_card_countRestricted, trunc_derivative, le_order_prod, Nat.Partition.multipliable_genFun, derivative_inv, derivativeFun_mul, derivative_X, Nat.Partition.genFun_eq_tprod, X_eq_normalizeX, derivative_pow, trunc_derivative'
|
instInhabited 📖 | CompOp | — |
instModule 📖 | CompOp | 190 mathmath: coeff_mul_eq_coeff_trunc_mul_trunc₂, CuspFormClass.qExpansion_isBigO, WithPiTopology.hasSum_iff_hasSum_coeff, hasSum_aeval, IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply, coeff_mul_one_sub_of_lt_order, coeff_mul_of_lt_order, IsRestricted.smul, 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, trunc_mul_trunc, trunc_X_pow_self_mul, derivative_exp, coeff_of_lt_order, coeff_succ_mul_X, gaussNorm_monomial, coeff_ne_zero_C, derivative_inv', Polynomial.coe_monomial, aeval_eq_sum, binomialSeries_coeff, coeff_subst, le_order_smul, coeff_coe, eq_shift_mul_X_pow_add_trunc, IsWeierstrassDivisorAt.coeff_seq_succ_sub_seq_mem, coeff_inv_aux, degree_trunc_lt, WithPiTopology.tendsto_iff_coeff_tendsto, coe_smul, WithPiTopology.uniformContinuous_coeff, coeff_zero_one, coeff_X_mul_largeSchroderSeriesSeries_sq, trunc_trunc_mul_trunc, coeff_invOfUnit, trunc_mul_C, hasSum_of_monomials_self, coeff_derivativeFun, eval₂_eq_tsum, trunc_X_of, instIsScalarTower, order_monomial, monomial_mul_monomial, eq_X_mul_shift_add_const, LaurentSeries.powerSeriesPart_coeff, IsWeierstrassDivisorAt.mod'_mk_eq_mod, coeff_invUnitsSub, prod_monomial, coeff_succ_C, trunc_trunc_mul, IsRestricted.isRestricted_iff, coeff_mk, Polynomial.coe_smul, sub_const_eq_X_mul_shift, coeff_largeSchroderSeries, HahnSeries.ofPowerSeries_apply_coeff, monomial_zero_eq_C, monomial_pow, eq_X_pow_mul_shift_add_trunc, trunc_trunc_of_le, ModularFormClass.qExpansion_coeff, coeff_exp, trunc_one_left, sub_const_eq_shift_mul_X, LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero, derivative_invOf, HasSubst.monomial', IsWeierstrassDivisorAt.isUnit_shift, Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval, constantCoeff_divXPowOrder, monomial_eq_mk, HahnSeries.toPowerSeriesAlg_symm_apply_coeff, trunc_C, ModularFormClass.qExpansion_coeff_zero, X_eq, coeff_comp_monomial, trunc_trunc_pow, coeff_mul, HahnSeries.coeff_toPowerSeries, IsWeierstrassDivisorAt.coeff_seq_mem, coeff_smul, coeff_monomial_same, trunc_apply, coeff_monomial, coeff_X, HahnSeries.coeff_toPowerSeries_symm, IsWeierstrassDivisorAt.coeff_div, as_tsum, derivative_coe, coeff_zero_eq_constantCoeff_apply, HahnSeries.ofPowerSeriesAlg_apply_coeff, Polynomial.IsDistinguishedAt.algEquivQuotient_symm_apply, ModularFormClass.hasSum_qExpansion_of_abs_lt, coeff_map, constantCoeff_smul, 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_zero_eq_constantCoeff, LaurentSeries.coeff_zero_of_lt_intValuation, X_pow_eq, monomial_eq_C_mul_X_pow, coeff_divXPowOrder, trunc_one, HahnSeries.SummableFamily.powerSeriesFamily_of_orderTop_pos, ext_iff, coeff_X_pow_self, trunc_succ, ModularFormClass.qExpansion_isBigO, coeff_mul_eq_coeff_trunc_mul_trunc, qExpansion_mul_coeff_zero, trunc_coe_eq_self, coeff_derivative, coeff_subst_finite, coeff_X_pow, ModularFormClass.hasSum_qExpansion_of_norm_lt, expand_monomial, qExpansion_coeff_unique, coeff_subst', derivative_subst, IsRestricted.monomial, coeff_expand, eval₂_trunc_eq_sum_range, trunc_one_X, coeff_succ_X_mul, IsWeierstrassDivisorAt.mk_mod'_eq_self, trunc_trunc, coeff_C_mul, X_pow_dvd_iff, derivative_C, order_eq, coeff_zero_X_mul, WithPiTopology.tendsto_trunc_atTop, coeff_C_mul_X_pow, coeff_X_pow_mul', coeff_pow, coeff_one_pow, coeff_mul_X_pow, smul_eq_C_mul, ModularFormClass.qExpansionFormalMultilinearSeries_coeff, trunc_sub, IsWeierstrassDivisorAt.seq_one, Nat.Partition.coeff_genFun, trunc_derivativeFun, coeff_subst_finite', trunc_map, coeff_coe_trunc_of_lt, trunc_zero', coeff_mul_prod_one_sub_of_lt_order, HahnSeries.toPowerSeries_symm_apply_coeff, trunc_derivative, LaurentSeries.coeff_coe_powerSeries, ModularFormClass.hasSum_qExpansion, qExpansion_coeff_isBigO_of_norm_isBigO, ModularFormClass.qExpansion_coeff_eq_intervalIntegral, coeff_one_mul, monomial_zero_eq_C_apply, Polynomial.coeff_coe, derivative_inv, natDegree_trunc_lt, trunc_X, derivative_X, IsWeierstrassDivisorAt.coeff_div_sub_seq_mem, coeff_X_pow_mul, coeff_zero_mul_X, order_monomial_of_ne_zero, trunc_C_mul, WithPiTopology.summable_iff_summable_coeff, hasSum_eval₂, coeff_one_X, derivative_pow, order_eq_nat, coeff_zero_X, IsWeierstrassDivisionAt.coeff_f_sub_r_mem, trunc_derivative'
|
instRing 📖 | CompOp | 10 mathmath: IsWeierstrassFactorizationAt.algEquivQuotient_apply, IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply, IsRestricted.add, IsWeierstrassDivisorAt.mod'_mk_eq_mod, LaurentSeries.powerSeriesEquivSubring_apply, Polynomial.IsDistinguishedAt.algEquivQuotient_symm_apply, WithPiTopology.instIsTopologicalRing, IsWeierstrassDivisorAt.mk_mod'_eq_self, binomialSeries_nat, Polynomial.IsDistinguishedAt.algEquivQuotient_apply
|
instSemiring 📖 | CompOp | 317 mathmath: IsWeierstrassFactorizationAt.algEquivQuotient_apply, hasSum_aeval, IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply, Polynomial.eval₂_C_X_eq_coe, constantCoeff_expand, coeff_mul_C, heval_C, coeff_rescale, invOneSubPow_zero, qExpansionRingHom_apply, coeff_expand_mul, expand_apply, MvPowerSeries.rescaleUnit, trunc_X_pow_self_mul, invOneSubPow_inv_eq_one_sub_pow, LaurentSeries.LaurentSeriesRingEquiv_def, algebraMap_apply'', spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_isPrime, order_expand, eq_divided_by_X_pow_order_Iff_Unit, Unit_of_divided_by_X_pow_order_zero, degree_weierstrassMod_lt, HahnSeries.ofPowerSeries_X_pow, coeff_ne_zero_C, mapAlgHom_apply, derivative_inv', instIsDomain, rescale_X, Nat.Partition.tendsto_order_genFun_term_atTop_nhds_top, coe_add, catalanSeries_constantCoeff, coeff_heval, isUnit_exp, aeval_eq_sum, LaurentSeries.ofPowerSeries_powerSeriesPart, LaurentSeries.single_order_mul_powerSeriesPart, Polynomial.coe_C, Polynomial.bernoulli_generating_function, isUnit_divided_by_X_pow_order, map_cos, coeff_coe, constantCoeff_X, eq_shift_mul_X_pow_add_trunc, LaurentSeries.coe_algebraMap, support_expand_subset, RatFunc.coe_coe, isUnit_iff_constantCoeff, subst_pow, WithPiTopology.continuous_constantCoeff, derivativeFun_smul, support_expand, IsWeierstrassFactorization.isWeierstrassDivision, smul_weierstrassDiv, coe_smul, coeff_X_mul_largeSchroderSeriesSeries_sq, LaurentSeries.val_le_one_iff_eq_coe, constantCoeff_invUnitsSub, mk_add_choose_mul_one_sub_pow_eq_one, rescale_rescale, coe_mul, trunc_mul_C, IsWeierstrassDivisionAt.degree_lt, rescale_zero_apply, commute_X_pow, substAlgHom_X, IsWeierstrassFactorizationAt.natDegree_eq_toNat_order_map_of_ne_top, heval_apply, Nat.Partition.hasProd_powerSeriesMk_card_countRestricted, coe_sub, mk_one_pow_eq_mk_choose_add, expand_one_apply, rescale_zero, le_order_map, rescale_mk, HasSubst.X_pow, constantCoeff_surj, largeSchroderSeries_eq_one_add_X_mul_largeSchroderSeries_add_X_mul_largeSchroderSeries_sq, substAlgHom_comp_substAlgHom, exp_mul_exp_neg_eq_one, constantCoeff_one, map_sin, derivativeFun_C, constantCoeff_invOfUnit, Polynomial.constantCoeff_coe, HasSubst.smul_X', expand_smul, C_injective, Nat.Partition.summable_genFun_term, eq_X_mul_shift_add_const, constantCoeff_comp_C, exp_mul_exp_eq_exp_add, IsWeierstrassDivisorAt.mod'_mk_eq_mod, evalNegHom_X, X_pow_mul, coeff_succ_C, IsWeierstrassFactorization.natDegree_eq_toNat_order_map, WithPiTopology.instIsTopologicalSemiring, Nat.Partition.powerSeriesMk_card_restricted_eq_tprod, invOneSubPow_inv_zero_eq_one, smul_weierstrassMod, exp_pow_sum, one_le_order_iff_constCoeff_eq_zero, HahnSeries.SummableFamily.powerSeriesFamily_hsum_zero, sub_const_eq_X_mul_shift, constantCoeff_C, Polynomial.coe_add, constantCoeff_inv, isWeierstrassFactorizationAt_iff, HahnSeries.ofPowerSeries_apply_coeff, LaurentSeries.of_powerSeries_localization, invUnitsSub_mul_sub, X_irreducible, monomial_zero_eq_C, monomial_pow, instNontrivialSubalgebra, eq_X_pow_mul_shift_add_trunc, WithPiTopology.isTopologicallyNilpotent_iff_constantCoeff_isNilpotent, map_eq_zero, HahnSeries.ofPowerSeries_X, isUnit_weierstrassUnit, one_sub_pow_add_mul_invOneSubPow_val_eq_one_sub_pow, LaurentSeries.coe_X_compare, not_isField, sub_const_eq_shift_mul_X, LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero, IsWeierstrassFactorizationAt.isUnit, coe_divXPowOrderHom, derivative_invOf, one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val, coe_zero, IsWeierstrassDivisorAt.isUnit_shift, map_X, Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval, map_comp, constantCoeff_divXPowOrder, HahnSeries.toPowerSeriesAlg_apply, inv_eq_zero, HahnSeries.toPowerSeriesAlg_symm_apply_coeff, LaurentSeries.exists_powerSeries_of_memIntegers, trunc_C, Nat.Partition.hasProd_powerSeriesMk_card_restricted, WithPiTopology.continuous_C, coe_C, coe_neg, min_order_le_order_add, gaussNorm_C, map_subst, expand_C, map_algebraMap_eq_subst_X, trunc_trunc_pow, constantCoeff_largeSchroderSeries, C_eq_algebraMap, HahnSeries.coeff_toPowerSeries, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, invOfUnit_eq, map_surjective, map_invUnitsSub, isNoetherianRing, le_order_pow, constantCoeff_divXPowOrder_eq_zero_iff, X_pow_mul_injective, expand_mul, IsWeierstrassDivisorAt.mod_smul, HahnSeries.coeff_toPowerSeries_symm, constantCoeff_zero, expand_mul_eq_comp, invOneSubPow_add, fg_iff_of_isPrime, Polynomial.coeToPowerSeries.algHom_apply, order_pow, LaurentSeries.powerSeriesRingEquiv_coe_apply, Nat.Partition.powerSeriesMk_card_countRestricted_eq_tprod, Unit_of_divided_by_X_pow_order_nonzero, coeff_zero_eq_constantCoeff_apply, HahnSeries.ofPowerSeriesAlg_apply_coeff, LaurentSeries.powerSeriesEquivSubring_apply, Polynomial.IsDistinguishedAt.algEquivQuotient_symm_apply, coeff_map, eval₂_C, constantCoeff_smul, heval_X, comp_aeval, constantCoeff_mk, eq_shift_mul_X_add_const, coeff_mul_X_pow', coeff_zero_C, Polynomial.algebraMap_hahnSeries_apply, coeff_C, coeff_inv, rescale_injective, Polynomial.coeToPowerSeries.ringHom_apply, map_expand, coeff_expand_of_not_dvd, LaurentSeries.powerSeriesEquivSubring_coe_apply, coe_eval₂Hom, coeff_zero_eq_constantCoeff, coe_X, invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos, exp_pow_eq_rescale_exp, X_pow_eq, monomial_eq_C_mul_X_pow, mul_X_pow_injective, Nat.Partition.summable_genFun_term', Nat.Partition.multipliable_powerSeriesMk_card_restricted, divXPowOrder_pow, HasSubst.comp, X_pow_order_dvd, ker_coeff_eq_max_ideal, algebraMap_eq, coeff_X_pow_self, continuous_aeval, map_C, heval_unit, invOneSubPow_eq_inv_one_sub_pow, IsWeierstrassFactorization.degree_eq_coe_lift_order_map, rescale_neg_one_X, constantCoeff_exp, coe_orderHom, catalanSeries_sq_mul_X_add_one, coeff_X_pow, IsWeierstrassFactorizationAt.degree_eq_coe_lift_order_map_of_ne_top, expand_monomial, isWeierstrassDivisionAt_iff, coeff_subst', instIsLocalRing, constantCoeff_toSubring, C_inv, coeff_expand, algebraMap_apply, coe_aeval, derivativeFun_add, HahnSeries.ofPowerSeries_apply, expand_one, X_pow_order_mul_divXPowOrder, map_exp, coe_one, IsWeierstrassDivisorAt.mk_mod'_eq_self, span_X_isPrime, invOneSubPow_val_one_eq_invUnitSub_one, inv_eq_inv_aux, aeval_coe, Nat.Partition.hasProd_genFun, coeff_heval_zero, order_ne_zero_iff_constCoeff_eq_zero, HahnSeries.ofPowerSeries_injective, IsWeierstrassFactorizationAt.smul, substAlgHom_coe, WithPiTopology.multipliable_one_add_of_tendsto_order_atTop_nhds_top, coeff_C_mul, X_pow_dvd_iff, derivative_C, X_pow_mul_inj, IsWeierstrassDivisorAt.div_smul, expand_X, X_dvd_iff, order_add_of_order_ne, invUnitsSub_mul_X, subst_smul, rescale_one, IsWeierstrassDivisionAt.smul, coeff_C_mul_X_pow, order_eq_emultiplicity_X, coeff_X_pow_mul', binomialSeries_nat, algebraMap_apply', HahnSeries.ofPowerSeries_C, coe_pow, substAlgHom_comp_substAlgHom_apply, weierstrassUnit_smul, coeff_pow, LaurentSeries.mem_integers_of_powerSeries, binomialSeries_constantCoeff, coeff_one_pow, HahnSeries.toPowerSeries_apply, coeff_mul_X_pow, smul_eq_C_mul, IsWeierstrassDivisorAt.seq_one, Nat.Partition.multipliable_powerSeriesMk_card_countRestricted, map_id, WithPiTopology.multipliable_one_sub_X_pow, order_X_pow, heval_mul, rescale_neg_one_invOneSubPow, HahnSeries.algebraMap_apply', coeff_subst_finite', trunc_map, smul_inv, qExpansion_of_pow, LaurentSeries.X_order_mul_powerSeriesPart, mul_X_pow_inj, qExpansion_smul, Polynomial.polynomial_map_coe, HahnSeries.toPowerSeries_symm_apply_coeff, LaurentSeries.coeff_coe_powerSeries, Polynomial.IsDistinguishedAt.algEquivQuotient_apply, order_add_of_order_eq, coeff_one_mul, monomial_zero_eq_C_apply, map_toSubring, Nat.Partition.multipliable_genFun, Polynomial.coe_pow, IsRestricted.C, HahnSeries.SummableFamily.powerSeriesFamily_smul, derivative_inv, derivativeFun_mul, coe_substAlgHom, rescale_mul, map.isLocalHom, invOneSubPow_val_succ_eq_mk_add_choose, coeff_X_pow_mul, map_injective, weierstrassDistinguished_smul, LaurentSeries.valuation_X_pow, Nat.Partition.genFun_eq_tprod, trunc_C_mul, instIsNoetherianRing, derivative_pow
|
instZero 📖 | CompOp | 46 mathmath: qExpansion_eq_zero_iff, zero_weierstrassDiv, IsWeierstrassDivisorAt.div_coe_eq_zero, zero_weierstrassMod, Unit_of_divided_by_X_pow_order_zero, Polynomial.coe_eq_zero_iff, Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_map, gaussNorm_zero, derivativeFun_C, weierstrassDiv_zero, X_inv, order_zero, weierstrassDiv_zero_right, HasSubst.zero', WithPiTopology.isTopologicallyNilpotent_iff_constantCoeff_isNilpotent, map_eq_zero, coe_zero, zero_inv, inv_eq_zero, weierstrassMod_zero_left, instNoZeroDivisors, derivativeFun_one, constantCoeff_divXPowOrder_eq_zero_iff, constantCoeff_zero, forall_coeff_eq_zero, IsWeierstrassDivisorAt.mod_zero, gaussNorm_eq_zero_iff, IsWeierstrassFactorization.degree_eq_coe_lift_order_map, IsWeierstrassFactorizationAt.degree_eq_coe_lift_order_map_of_ne_top, IsWeierstrassDivisorAt.eq_zero_of_mul_eq, WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_isNilpotent, Polynomial.coe_zero, order_eq_top, IsWeierstrassDivisorAt.div_zero, derivative_C, weierstrassMod_zero_right, weierstrassMod_zero, qExpansion_zero, WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_zero, weierstrassDiv_zero_left, LaurentSeries.powerSeriesPart_zero, IsWeierstrassDivisorAt.seq_zero, isWeierstrassDivisionAt_zero, divXPowOrder_zero, IsRestricted.zero, LaurentSeries.powerSeriesPart_eq_zero
|
map 📖 | CompOp | 36 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, IsWeierstrassFactorization.natDegree_eq_toNat_order_map, map_eq_zero, 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, 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 | 15 mathmath: coeff_rescale, MvPowerSeries.rescaleUnit, rescale_X, Polynomial.bernoulli_generating_function, rescale_rescale, rescale_zero_apply, rescale_zero, rescale_mk, exp_mul_exp_eq_exp_add, rescale_injective, exp_pow_eq_rescale_exp, rescale_neg_one_X, rescale_one, rescale_neg_one_invOneSubPow, rescale_mul
|
toSubring 📖 | CompOp | 4 mathmath: coeff_toSubring, order_toSubring, constantCoeff_toSubring, map_toSubring
|
«term_⟦X⟧» 📖 | CompOp | — |