| Name | Category | Theorems |
|---|
C 📖 | CompOp | 30 mathmath: MvPolynomial.coe_C, subst_C, smul_eq_C_mul, trunc_C, constantCoeff_C, monomial_zero_eq_C, constantCoeff_comp_C, rename_C, c_eq_algebraMap, truncFinset_C, C_inv, monomial_zero_eq_C_apply, coeff_C_mul, PowerSeries.subst_C, rescale_zero, coeff_zero_C, coeff_C, algebraMap_apply, eval₂_C, trunc_C_mul, map_C, killCompl_C, rescale_zero_apply, monomial_smul_eq, monomial_eq', coeff_mul_C, expand_C, trunc'_C, trunc'_C_mul, WithPiTopology.continuous_C
|
X 📖 | CompOp | 45 mathmath: coeff_X_pow, X_pow_mul, eval₂_X, commute_X_pow, X_pow_eq, map_algebraMap_eq_subst_X, substAlgHom_X, coeff_X, X_pow_dvd_iff, coeff_index_single_X, X_def, MvPolynomial.coe_X, commute_X, coeff_index_single_self_X, coeff_zero_mul_X, PowerSeries.HasSubst.X, HasSubst.X_pow, X_inj, X_mul, coeff_zero_X_mul, subst_X, X_dvd_iff, rescale_eq_subst, killCompl_X_eq_zero, constantCoeff_X, HasSubst.smul_X, HasEval.X, expand_X, X_inv, coeff_zero_X, HasSubst.X, monomial_one_eq, monomial_eq, X_mem_nonzeroDivisors, WithPiTopology.variables_tendsto_zero, map_X, killCompl_X, rename_X, monomial_smul_const, subst_self, PowerSeries.HasSubst.smul_X, monomial_smul_eq, aeval_unique, monomial_eq', prod_smul_X_eq_smul_monomial_one
|
algebraMvPolynomial 📖 | CompOp | 1 mathmath: algebraMap_apply'
|
algebraMvPowerSeries 📖 | CompOp | 1 mathmath: algebraMap_apply''
|
coeff 📖 | CompOp | 98 mathmath: coeff_zero_eq_constantCoeff_apply, hasSubst_def, coeff_zero_eq_constantCoeff, coeff_zero, coeff_mul_monomial, coeff_pow, constantCoeff_subst, coeff_monomial_mul, coeff_X_pow, coeff_mul_right_one_sub_of_lt_weightedOrder, PowerSeries.coeff_subst, coeff_eq_zero_of_constantCoeff_nilpotent, coeff_X, coeff_monomial_same, hasSum_aeval, coeff_truncFinset_of_mem, X_pow_dvd_iff, coeff_mul_prod_one_sub_of_lt_order, coeff_index_single_X, LinearTopology.mem_basis_iff, coeff_of_lt_order, coeff_embDomain_rename, ext_iff, WithPiTopology.continuous_coeff, coeff_trunc'_mul_trunc'_eq_coeff_mul, le_lexOrder_iff, coeff_index_single_self_X, WithPiTopology.as_tsum, WithPiTopology.uniformContinuous_coeff, coeff_inv, coeff_homogeneousComponent, WithPiTopology.hasSum_iff_hasSum_coeff, coeff_subst, HasSubst.coeff_zero, coeff_one, coeff_truncFinset_mul_truncFinset_eq_coeff_mul, coeff_mul_right_one_sub_of_lt_order, coeff_expand_smul, eval₂_eq_tsum, le_weightedOrder_subst, coeff_comp_monomial, MvPolynomial.coeff_coe, coeff_trunc', coeff_zero_mul_X, coeff_inv_aux, coeff_weightedHomogeneousComponent, coeff_apply, coeff_trunc, eq_zero_iff_forall_coeff_eq_zero_and, coeff_prod, coeff_C_mul, coeff_zero_one, PowerSeries.coeff_def, coeff_add_mul_monomial, coeff_zero_X_mul, coeff_zero_iff, coeff_mul_left_one_sub_of_lt_weightedOrder, weightedOrder_eq_nat, coeff_rescale, WithPiTopology.hasSum_of_monomials_self, eq_zero_iff_forall_coeff_zero, HahnSeries.coeff_toMvPowerSeries_symm, coeff_expand_of_not_dvd, coeff_zero_C, coeff_monomial, X_dvd_iff, coeff_C, WithPiTopology.summable_iff_summable_coeff, coeff_invOfUnit, coeff_map, coeff_toSubring, coeff_mul_eq_coeff_trunc'_mul_trunc', coeff_smul, coeff_zero_X, HahnSeries.coeff_toMvPowerSeries, PowerSeries.coeff_subst_finite, coeff_killCompl, aeval_eq_sum, coeff_monomial_ne, coeff_truncFinset, coeff_subst_finite, order_eq_nat, IsWeightedHomogeneous.coeff_eq_zero, coeff_rename_eq_zero, coeff_mul_left_one_sub_of_lt_order, coeff_rename, WithPiTopology.tendsto_iff_coeff_tendsto, hasSum_eval₂, truncFinset_apply, IsHomogeneous.coeff_eq_zero, coeff_eq_zero_of_lt_lexOrder, coeff_mul_of_add_lexOrder, coeff_eq_zero_of_lt_weightedOrder, coeff_mul_C, coeff_mul, coeff_mul_prod_one_sub_of_lt_weightedOrder, coeff_add_monomial_mul, commute_monomial
|
constantCoeff 📖 | CompOp | 33 mathmath: coeff_zero_eq_constantCoeff_apply, hasSubst_def, coeff_zero_eq_constantCoeff, PowerSeries.constantCoeff_subst, constantCoeff_subst, WithPiTopology.isTopologicallyNilpotent_iff_constantCoeff_isNilpotent, isUnit_iff_constantCoeff, LinearTopology.isTopologicallyNilpotent_iff_constantCoeff, one_le_order_iff_constCoeff_eq_zero, constantCoeff_invOfUnit, constantCoeff_inv, constantCoeff_C, coeff_inv, constantCoeff_comp_C, constantCoeff_smul, HasSubst.const_coeff, constantCoeff_zero, PowerSeries.constantCoeff_subst_eq_zero, constantCoeff_toSubring, rescale_zero, constantCoeff_subst_eq_zero, isUnit_constantCoeff, inv_eq_zero, constantCoeff_rename, constantCoeff_one, order_ne_zero_iff_constCoeff_eq_zero, constantCoeff_map, constantCoeff_X, constantCoeff_expand, IsNilpotent_subst, invOfUnit_eq, rescale_zero_apply, WithPiTopology.continuous_constantCoeff
|
instAddCommGroup 📖 | CompOp | 18 mathmath: PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply, PowerSeries.derivative_inv', LinearTopology.instIsLinearTopologyMulOpposite, PowerSeries.IsWeierstrassDivisorAt.mod'_mk_eq_mod, PowerSeries.evalNegHom_X, PowerSeries.IsRestricted.neg, PowerSeries.derivative_invOf, LinearTopology.instIsLinearTopologyOfMulOpposite, PowerSeries.coe_neg, weightedOrder_neg, Polynomial.IsDistinguishedAt.algEquivQuotient_symm_apply, Polynomial.coe_neg, qExpansion_neg, PowerSeries.rescale_neg_one_X, PowerSeries.order_neg, order_neg, PowerSeries.IsWeierstrassDivisorAt.mk_mod'_eq_self, PowerSeries.derivative_inv
|
instAddCommMonoid 📖 | CompOp | 387 mathmath: PowerSeries.coeff_mul_eq_coeff_trunc_mul_trunc₂, coeff_zero_eq_constantCoeff_apply, PowerSeries.coeff_toSubring, CuspFormClass.qExpansion_isBigO, hasSubst_def, PowerSeries.WithPiTopology.hasSum_iff_hasSum_coeff, WithPiTopology.tendsto_trunc_atTop, PowerSeries.hasSum_aeval, coeff_zero_eq_constantCoeff, PowerSeries.coeff_mul_one_sub_of_lt_order, coeff_zero, weightedOrder_monomial, eq_iff_frequently_trunc'_eq, PowerSeries.coeff_mul_of_lt_order, PowerSeries.IsRestricted.smul, PowerSeries.coeff_of_lt_order_toNat, PowerSeries.constantCoeff_subst, truncFinset_one, PowerSeries.WithPiTopology.continuous_coeff, trunc'_trunc', ModularFormClass.qExpansionFormalMultilinearSeries_apply_norm, PowerSeries.coeff_mul_C, coeff_mul_monomial, PowerSeries.coeff_rescale, PowerSeries.coeff_expand_mul, PowerSeries.catalanSeries_coeff, PowerSeries.coeff_X_mul_largeSchroderSeries, PowerSeries.coeff_trunc, PowerSeries.trunc_mul_trunc, PowerSeries.trunc_X_pow_self_mul, coeff_pow, PowerSeries.derivative_exp, PowerSeries.coeff_of_lt_order, constantCoeff_subst, trunc'_expand_trunc', PowerSeries.coeff_succ_mul_X, coeff_monomial_mul, PowerSeries.coeff_mul_mem_ideal_of_coeff_right_mem_ideal', coeff_X_pow, PowerSeries.gaussNorm_monomial, X_pow_eq, ext_trunc', WithPiTopology.summable_of_tendsto_order_atTop_nhds_top, PowerSeries.coeff_ne_zero_C, monomial_mem_nonzeroDivisors, PowerSeries.derivative_inv', coeff_mul_right_one_sub_of_lt_weightedOrder, Polynomial.coe_monomial, PowerSeries.aeval_eq_sum, PowerSeries.binomialSeries_coeff, monomial_mem_nonzeroDivisorsLeft, smul_eq_C_mul, trunc_C, PowerSeries.coeff_subst, PowerSeries.le_order_smul, coeff_eq_zero_of_constantCoeff_nilpotent, PowerSeries.coeff_coe, coeff_X, PowerSeries.eq_shift_mul_X_pow_add_trunc, PowerSeries.IsWeierstrassDivisorAt.coeff_seq_succ_sub_seq_mem, coeff_monomial_same, hasSum_aeval, coeff_truncFinset_of_mem, weightedOrder_monomial_of_ne_zero, PowerSeries.coeff_inv_aux, X_pow_dvd_iff, PowerSeries.degree_trunc_lt, coeff_mul_prod_one_sub_of_lt_order, PowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto, PowerSeries.coe_smul, coeff_index_single_X, PowerSeries.WithPiTopology.uniformContinuous_coeff, LinearTopology.mem_basis_iff, subst_monomial, PowerSeries.coeff_zero_one, coeff_of_lt_order, PowerSeries.coeff_X_mul_largeSchroderSeriesSeries_sq, trunc'_trunc'_pow, coeff_embDomain_rename, MvPolynomial.coe_monomial, X_def, ext_iff, trunc_one, PowerSeries.trunc_trunc_mul_trunc, PowerSeries.coeff_invOfUnit, WithPiTopology.continuous_coeff, PowerSeries.trunc_mul_C, PowerSeries.hasSum_of_monomials_self, coeff_trunc'_mul_trunc'_eq_coeff_mul, le_lexOrder_iff, Nat.Partition.hasProd_powerSeriesMk_card_countRestricted, monomial_mem_nonzeroDivisorsRight, PowerSeries.coeff_derivativeFun, coeff_index_single_self_X, WithPiTopology.as_tsum, WithPiTopology.uniformContinuous_coeff, monomial_zero_eq_C, coeff_inv, PowerSeries.eval₂_eq_tsum, PowerSeries.trunc_X_of, PowerSeries.WithPiTopology.summable_prod_of_tendsto_order_atTop_nhds_top, rename_monomial, PowerSeries.order_monomial, coeff_homogeneousComponent, PowerSeries.monomial_mul_monomial, weightedHomogeneousComponent_of_lt_weightedOrder_eq_zero, Nat.Partition.summable_genFun_term, WithPiTopology.hasSum_iff_hasSum_coeff, PowerSeries.eq_X_mul_shift_add_const, coeff_subst, constantCoeff_smul, killCompl_monomial_embDomain, LaurentSeries.powerSeriesPart_coeff, PowerSeries.coeff_invUnitsSub, PowerSeries.prod_monomial, PowerSeries.coeff_succ_C, PowerSeries.trunc_trunc_mul, truncFinset_C, HasSubst.coeff_zero, Nat.Partition.powerSeriesMk_card_restricted_eq_tprod, PowerSeries.IsRestricted.isRestricted_iff, PowerSeries.exp_pow_sum, coeff_one, truncFinset_map, PowerSeries.coeff_mul_mem_ideal_of_coeff_right_mem_ideal, PowerSeries.coeff_mk, coeff_truncFinset_mul_truncFinset_eq_coeff_mul, Polynomial.coe_smul, WithPiTopology.summable_pow_of_constantCoeff_eq_zero, PowerSeries.sub_const_eq_X_mul_shift, PowerSeries.coeff_largeSchroderSeries, coeff_mul_right_one_sub_of_lt_order, coeff_expand_smul, le_weightedOrder_smul, truncFinset_monomial_eq_zero, HahnSeries.ofPowerSeries_apply_coeff, eval₂_eq_tsum, homogeneousComponent_of_lt_order_eq_zero, le_weightedOrder_subst, trunc'_expand, monomial_zero_eq_C_apply, PowerSeries.monomial_zero_eq_C, PowerSeries.monomial_pow, coeff_comp_monomial, PowerSeries.eq_X_pow_mul_shift_add_trunc, PowerSeries.trunc_trunc_of_le, ModularFormClass.qExpansion_coeff, trunc_map, PowerSeries.coeff_exp, PowerSeries.trunc_one_left, isHomogeneous_iff_eq_homogeneousComponent, MvPolynomial.coeff_coe, coeff_trunc', PowerSeries.sub_const_eq_shift_mul_X, LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero, coeff_zero_mul_X, coeff_inv_aux, PowerSeries.WithPiTopology.one_sub_mul_tsum_pow_of_constantCoeff_eq_zero, WithPiTopology.one_sub_mul_tsum_pow_of_constantCoeff_eq_zero, coeff_weightedHomogeneousComponent, PowerSeries.derivative_invOf, PowerSeries.HasSubst.monomial', PowerSeries.IsWeierstrassDivisorAt.isUnit_shift, Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval, coeff_apply, PowerSeries.constantCoeff_divXPowOrder, PowerSeries.monomial_eq_mk, coeff_trunc, HahnSeries.toPowerSeriesAlg_symm_apply_coeff, eq_zero_iff_forall_coeff_eq_zero_and, PowerSeries.trunc_C, Nat.Partition.hasProd_powerSeriesMk_card_restricted, ModularFormClass.qExpansion_coeff_zero, WithPiTopology.summable_prod_of_tendsto_weightedOrder_atTop_nhds_top, coeff_prod, truncFinset_monomial, coeff_C_mul, PowerSeries.X_eq, weightedHomogeneousComponent_mul_of_le_weightedOrder, PowerSeries.coeff_comp_monomial, coeff_zero_one, PowerSeries.trunc_trunc_pow, PowerSeries.coeff_mul, add_mul, HahnSeries.coeff_toPowerSeries, PowerSeries.IsWeierstrassDivisorAt.coeff_seq_mem, PowerSeries.coeff_smul, coeff_add_mul_monomial, monomial_pow, PowerSeries.coeff_monomial_same, WithPiTopology.tsum_pow_mul_one_sub_of_constantCoeff_eq_zero, coeff_zero_X_mul, map_monomial, PowerSeries.trunc_apply, le_order_smul, PowerSeries.coeff_mul_mem_ideal_of_coeff_left_mem_ideal', PowerSeries.coeff_monomial, coeff_zero_iff, PowerSeries.coeff_X, HahnSeries.coeff_toPowerSeries_symm, PowerSeries.IsWeierstrassDivisorAt.coeff_div, EisensteinSeries.E_qExpansion_coeff, coeff_mul_left_one_sub_of_lt_weightedOrder, weightedOrder_eq_nat, totalDegree_trunc', PowerSeries.as_tsum, expand_monomial, Nat.Partition.powerSeriesMk_card_countRestricted_eq_tprod, PowerSeries.derivative_coe, PowerSeries.coeff_zero_eq_constantCoeff_apply, HahnSeries.ofPowerSeriesAlg_apply_coeff, ModularFormClass.hasSum_qExpansion_of_abs_lt, PowerSeries.coeff_map, PowerSeries.constantCoeff_smul, coeff_rescale, WithPiTopology.hasSum_of_monomials_self, PowerSeries.coeff_one, PowerSeries.eq_shift_mul_X_add_const, PowerSeries.coeff_prod, PowerSeries.coeff_mul_X_pow', PowerSeries.coeff_zero_C, eq_zero_iff_forall_coeff_zero, PowerSeries.forall_coeff_eq_zero, PowerSeries.coeff_C, HahnSeries.coeff_toMvPowerSeries_symm, isWeightedHomogeneous_weightedHomogeneousComponent, PowerSeries.coeff_inv, coeff_expand_of_not_dvd, coeff_zero_C, coeff_monomial, X_dvd_iff, coeff_C, ModularFormClass.qExpansion_coeff_eq_circleIntegral, PowerSeries.WithPiTopology.tsum_pow_mul_one_sub_of_constantCoeff_eq_zero, PowerSeries.coeff_expand_of_not_dvd, homogeneousComponent_mul_of_le_order, PowerSeries.coeff_subst_X_pow, PowerSeries.coeff_zero_eq_constantCoeff, WithPiTopology.summable_prod_of_tendsto_order_atTop_nhds_top, LaurentSeries.coeff_zero_of_lt_intValuation, WithPiTopology.summable_iff_summable_coeff, instIsScalarTower, PowerSeries.X_pow_eq, coeff_invOfUnit, coeff_map, coeff_toSubring, PowerSeries.monomial_eq_C_mul_X_pow, Nat.Partition.summable_genFun_term', Nat.Partition.multipliable_powerSeriesMk_card_restricted, coeff_mul_eq_coeff_trunc'_mul_trunc', killCompl_monomial_eq_zero, PowerSeries.le_gaussNorm, totalDegree_truncFinset, PowerSeries.coeff_divXPowOrder, PowerSeries.trunc_one, HahnSeries.SummableFamily.powerSeriesFamily_of_orderTop_pos, WithPiTopology.tendsto_trunc'_atTop, PowerSeries.ext_iff, PowerSeries.coeff_X_pow_self, PowerSeries.trunc_succ, coeff_smul, coeff_zero_X, ModularFormClass.qExpansion_isBigO, HahnSeries.coeff_toMvPowerSeries, PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal, order_monomial, PowerSeries.coeff_mul_eq_coeff_trunc_mul_trunc, substAlgHom_monomial, qExpansion_mul_coeff_zero, PowerSeries.trunc_coe_eq_self, coeff_truncFinset_eq_zero, PowerSeries.coeff_derivative, PowerSeries.coeff_subst_finite, PowerSeries.coeff_X_pow, isHomogeneous_homogeneousComponent, ModularFormClass.hasSum_qExpansion_of_norm_lt, coeff_killCompl, PowerSeries.expand_monomial, aeval_eq_sum, qExpansion_coeff_unique, PowerSeries.coeff_subst', PowerSeries.derivative_subst, monomial_zero_one, monomial_one_eq, PowerSeries.IsRestricted.monomial, PowerSeries.coeff_expand, PowerSeries.eval₂_trunc_eq_sum_range, PowerSeries.trunc_one_X, monomial_eq, PowerSeries.coeff_succ_X_mul, coeff_monomial_ne, PowerSeries.trunc_trunc, truncFinset_truncFinset, support_truncFinset_subset, coeff_truncFinset, Nat.Partition.hasProd_genFun, coeff_subst_finite, order_eq_nat, IsWeightedHomogeneous.coeff_eq_zero, PowerSeries.coeff_C_mul, PowerSeries.X_pow_dvd_iff, coeff_rename_eq_zero, PowerSeries.coeff_mul_mem_ideal_of_coeff_left_mem_ideal, coeff_mul_left_one_sub_of_lt_order, PowerSeries.derivative_C, coeff_rename, PowerSeries.order_eq, monomial_mul_monomial, PowerSeries.coeff_zero_X_mul, mul_add, EisensteinSeries.E_qExpansion_coeff_zero, PowerSeries.WithPiTopology.tendsto_trunc_atTop, PowerSeries.coeff_C_mul_X_pow, trunc'_one, trunc_C_mul, PowerSeries.coeff_X_pow_mul', WithPiTopology.tendsto_iff_coeff_tendsto, isWeightedHomogeneous_iff_eq_weightedHomogeneousComponent, PowerSeries.coeff_pow, PowerSeries.coeff_one_pow, monomial_smul_const, PowerSeries.coeff_mul_X_pow, trunc'_map, PowerSeries.smul_eq_C_mul, ModularFormClass.qExpansionFormalMultilinearSeries_coeff, PowerSeries.trunc_sub, hasSum_eval₂, PowerSeries.IsWeierstrassDivisorAt.seq_one, Nat.Partition.coeff_genFun, Nat.Partition.multipliable_powerSeriesMk_card_countRestricted, PowerSeries.trunc_derivativeFun, PowerSeries.WithPiTopology.summable_of_tendsto_order_atTop_nhds_top, PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal', PowerSeries.coeff_subst_finite', PowerSeries.HasSubst.monomial, PowerSeries.trunc_map, PowerSeries.coeff_coe_trunc_of_lt, PowerSeries.trunc_zero', PowerSeries.coeff_mul_prod_one_sub_of_lt_order, HahnSeries.toPowerSeries_symm_apply_coeff, PowerSeries.trunc_derivative, monomial_smul_eq, LaurentSeries.coeff_coe_powerSeries, truncFinset_apply, order_monomial_of_ne_zero, ModularFormClass.hasSum_qExpansion, IsHomogeneous.coeff_eq_zero, qExpansion_coeff_isBigO_of_norm_isBigO, ModularFormClass.qExpansion_coeff_eq_intervalIntegral, PowerSeries.coeff_one_mul, coeff_eq_zero_of_lt_lexOrder, PowerSeries.monomial_zero_eq_C_apply, coeff_mul_of_add_lexOrder, Nat.Partition.multipliable_genFun, Polynomial.coeff_coe, PowerSeries.derivative_inv, coeff_eq_zero_of_lt_weightedOrder, PowerSeries.natDegree_trunc_lt, PowerSeries.trunc_X, PowerSeries.derivative_X, PowerSeries.WithPiTopology.summable_pow_of_constantCoeff_eq_zero, monomial_eq', PowerSeries.IsWeierstrassDivisorAt.coeff_div_sub_seq_mem, PowerSeries.coeff_X_pow_mul, PowerSeries.coeff_zero_mul_X, coeff_mul_C, Nat.Partition.genFun_eq_tprod, PowerSeries.order_monomial_of_ne_zero, PowerSeries.trunc_C_mul, coeff_mul, PowerSeries.WithPiTopology.summable_iff_summable_coeff, coeff_mul_prod_one_sub_of_lt_weightedOrder, WithPiTopology.summable_of_tendsto_weightedOrder_atTop_nhds_top, coeff_add_monomial_mul, PowerSeries.hasSum_eval₂, trunc'_C, prod_monomial, prod_smul_X_eq_smul_monomial_one, PowerSeries.coeff_one_X, trunc'_C_mul, truncFinset_truncFinset_pow, commute_monomial, PowerSeries.derivative_pow, PowerSeries.order_eq_nat, PowerSeries.coeff_zero_X, PowerSeries.IsWeierstrassDivisionAt.coeff_f_sub_r_mem, PowerSeries.trunc_derivative'
|
instAddGroup 📖 | CompOp | 39 mathmath: PowerSeries.coeff_mul_one_sub_of_lt_order, PowerSeries.invOneSubPow_inv_eq_one_sub_pow, coeff_mul_right_one_sub_of_lt_weightedOrder, PowerSeries.subst_sub, Polynomial.bernoulli_generating_function, bernoulliPowerSeries_mul_exp_sub_one, PowerSeries.IsWeierstrassDivisorAt.coeff_seq_succ_sub_seq_mem, coeff_mul_prod_one_sub_of_lt_order, PowerSeries.mk_add_choose_mul_one_sub_pow_eq_one, PowerSeries.coe_sub, bernoulli'PowerSeries_mul_exp_sub_one, LaurentSeries.exists_Polynomial_intValuation_lt, PowerSeries.sub_const_eq_X_mul_shift, coeff_mul_right_one_sub_of_lt_order, PowerSeries.invUnitsSub_mul_sub, WithPiTopology.instIsUniformAddGroup, PowerSeries.one_sub_pow_add_mul_invOneSubPow_val_eq_one_sub_pow, PowerSeries.sub_const_eq_shift_mul_X, qExpansion_sub, PowerSeries.WithPiTopology.one_sub_mul_tsum_pow_of_constantCoeff_eq_zero, WithPiTopology.one_sub_mul_tsum_pow_of_constantCoeff_eq_zero, PowerSeries.one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val, PowerSeries.IsWeierstrassDivisorAt.coeff_seq_mem, WithPiTopology.tsum_pow_mul_one_sub_of_constantCoeff_eq_zero, coeff_mul_left_one_sub_of_lt_weightedOrder, PowerSeries.WithPiTopology.instIsUniformAddGroup, Polynomial.coe_sub, PowerSeries.WithPiTopology.tsum_pow_mul_one_sub_of_constantCoeff_eq_zero, PowerSeries.invOneSubPow_eq_inv_one_sub_pow, subst_sub, coeff_mul_left_one_sub_of_lt_order, PowerSeries.invUnitsSub_mul_X, PowerSeries.trunc_sub, PowerSeries.WithPiTopology.multipliable_one_sub_X_pow, PowerSeries.coeff_mul_prod_one_sub_of_lt_order, PowerSeries.mk_one_mul_one_sub_eq_one, PowerSeries.IsWeierstrassDivisorAt.coeff_div_sub_seq_mem, coeff_mul_prod_one_sub_of_lt_weightedOrder, PowerSeries.IsWeierstrassDivisionAt.coeff_f_sub_r_mem
|
instAddMonoid 📖 | CompOp | 13 mathmath: PowerSeries.IsRestricted.smul, smul_eq_C_mul, PowerSeries.le_order_smul, PowerSeries.coe_smul, constantCoeff_smul, Polynomial.coe_smul, le_weightedOrder_smul, PowerSeries.coeff_smul, le_order_smul, PowerSeries.constantCoeff_smul, instIsScalarTower, coeff_smul, PowerSeries.smul_eq_C_mul
|
instAddMonoidWithOne 📖 | CompOp | 1 mathmath: PowerSeries.derivative_pow
|
instAlgebra 📖 | CompOp | 183 mathmath: PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_apply, PowerSeries.hasSum_aeval, PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply, PowerSeries.rescale_eq_subst, PowerSeries.constantCoeff_expand, PowerSeries.heval_C, support_expand, subst_eq_eval₂, PowerSeries.coeff_expand_mul, PowerSeries.expand_subst, PowerSeries.expand_apply, PowerSeries.derivative_exp, PowerSeries.order_expand, mapAlgHom_apply, PowerSeries.HasSubst.smul', substAlgHom_X, continuous_aeval, PowerSeries.mapAlgHom_apply, PowerSeries.derivative_inv', coe_substAlgHom, Nat.Partition.tendsto_order_genFun_term_atTop_nhds_top, rename_map, PowerSeries.coeff_heval, PowerSeries.aeval_eq_sum, expand_mul, killCompl_comp_rename, expand_substAlgHom, PowerSeries.support_expand_subset, substAlgHom_eq_aeval, hasSum_aeval, PowerSeries.derivativeFun_smul, PowerSeries.support_expand, PowerSeries.smul_weierstrassDiv, comp_aeval, subst_monomial, coeff_embDomain_rename, renameEquiv_symm, WithPiTopology.instContinuousSMul, PowerSeries.substAlgHom_X, expand_one_apply, PowerSeries.heval_apply, PowerSeries.expand_one_apply, LaurentSeries.algebraMap_apply, rename_rename, PowerSeries.aeval_unique, PowerSeries.substAlgHom_comp_substAlgHom, HasSubst.comp, rename_C, rename_monomial, PowerSeries.HasSubst.smul_X', PowerSeries.expand_smul, rescaleAlgHom_one, c_eq_algebraMap, rename_id, Nat.Partition.summable_genFun_term, expand_eq_expand, substAlgHom_comp_substAlgHom_apply, killCompl_monomial_embDomain, PowerSeries.IsWeierstrassDivisorAt.mod'_mk_eq_mod, rescaleAlgHom_mul, expand_one, PowerSeries.smul_weierstrassMod, coeff_expand_smul, rename_id_apply, aeval_coe, trunc'_expand, PowerSeries.instNontrivialSubalgebra, comp_subst_apply, rename_coe, PowerSeries.derivative_invOf, instNontrivialSubalgebraOfNonempty, HahnSeries.toPowerSeriesAlg_apply, HahnSeries.toPowerSeriesAlg_symm_apply_coeff, expand_subst, killCompl_rename_app, rename_inj, substAlgHom_coe, rescale_homogeneous_eq_smul, PowerSeries.expand_C, killCompl_map, PowerSeries.C_eq_algebraMap, expand_comp_substAlgHom, PowerSeries.subst_coe, MvPolynomial.coeToMvPowerSeries.algHom_apply, rename_comp_rename, PowerSeries.expand_mul, PowerSeries.IsWeierstrassDivisorAt.mod_smul, PowerSeries.expand_mul_eq_comp, Polynomial.coeToPowerSeries.algHom_apply, expand_monomial, PowerSeries.derivative_coe, order_expand, HahnSeries.ofPowerSeriesAlg_apply_coeff, map_iterateFrobenius_expand, Polynomial.IsDistinguishedAt.algEquivQuotient_symm_apply, MvPolynomial.coe_smul, PowerSeries.heval_X, PowerSeries.comp_aeval, constantCoeff_rename, renameEquiv_refl, coeff_expand_of_not_dvd, PowerSeries.map_expand, rescaleAlgHom_apply, PowerSeries.coeff_expand_of_not_dvd, rescale_eq_subst, coe_aeval, killCompl_X_eq_zero, rename_injective, HasSubst.smul_X, map_frobenius_expand, Nat.Partition.summable_genFun_term', expand_X, map_expand, PowerSeries.HasSubst.comp, killCompl_monomial_eq_zero, renameEquiv_apply, PowerSeries.algebraMap_eq, constantCoeff_expand, PowerSeries.continuous_aeval, PowerSeries.heval_unit, substAlgHom_monomial, algebraMap_apply, PowerSeries.coeff_derivative, coeff_killCompl, PowerSeries.expand_monomial, aeval_eq_sum, PowerSeries.derivative_subst, IsNilpotent_subst, PowerSeries.coeff_expand, PowerSeries.algebraMap_apply, PowerSeries.coe_aeval, comp_subst, PowerSeries.expand_one, monomial_eq, PowerSeries.IsWeierstrassDivisorAt.mk_mod'_eq_self, PowerSeries.substAlgHom_eq_aeval, PowerSeries.coe_rescaleAlgHom, PowerSeries.aeval_coe, Nat.Partition.hasProd_genFun, PowerSeries.coeff_heval_zero, PowerSeries.IsWeierstrassFactorizationAt.smul, PowerSeries.substAlgHom_coe, coeff_rename_eq_zero, PowerSeries.derivative_C, PowerSeries.IsWeierstrassDivisorAt.div_smul, coeff_rename, subst_smul, support_expand_subset, PowerSeries.expand_X, PowerSeries.subst_smul, PowerSeries.IsWeierstrassDivisionAt.smul, killCompl_X, rename_X, PowerSeries.substAlgHom_comp_substAlgHom_apply, PowerSeries.weierstrassUnit_smul, killCompl_C, monomial_smul_const, expand_mul_eq_comp, PowerSeries.heval_mul, comp_substAlgHom, PowerSeries.smul_inv, qExpansion_smul, PowerSeries.HasSubst.smul_X, PowerSeries.trunc_derivative, Polynomial.IsDistinguishedAt.algEquivQuotient_apply, subst_coe, smul_inv, substAlgHom_apply, Nat.Partition.multipliable_genFun, substAlgHom_comp_substAlgHom, HahnSeries.SummableFamily.powerSeriesFamily_smul, PowerSeries.derivative_inv, aeval_unique, HasSubst.expand, PowerSeries.coe_substAlgHom, PowerSeries.derivative_X, PowerSeries.weierstrassDistinguished_smul, Nat.Partition.genFun_eq_tprod, renameEquiv_trans, expand_C, prod_smul_X_eq_smul_monomial_one, PowerSeries.derivative_pow, PowerSeries.trunc_derivative'
|
instCommRing 📖 | CompOp | 54 mathmath: PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_apply, HahnSeries.SummableFamily.powerSeriesFamily_add, PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply, subst_eq_eval₂, PowerSeries.eq_mul_weierstrassDiv_add_weierstrassMod, constantCoeff_subst, subst_add, substAlgHom_eq_aeval, coeff_mul_prod_one_sub_of_lt_order, subst_monomial, PowerSeries.intValuation_eq_of_coe, PowerSeries.IsWeierstrassDivisionAt.eq_mul_add, PowerSeries.aeval_unique, coeff_subst, PowerSeries.IsWeierstrassDivisorAt.mod'_mk_eq_mod, LaurentSeries.exists_Polynomial_intValuation_lt, RatFunc.valuation_eq_LaurentSeries_valuation, comp_subst_apply, PowerSeries.IsWeierstrassDivisorAt.mod_add, hasSubst_iff_hasEval_of_discreteTopology, PowerSeries.hasUnitMulPowIrreducibleFactorization, qExpansion_add, PowerSeries.instIsDiscreteValuationRing, PowerSeries.subst_add, LaurentSeries.powerSeriesRingEquiv_coe_apply, LaurentSeries.powerSeriesEquivSubring_apply, Polynomial.IsDistinguishedAt.algEquivQuotient_symm_apply, PowerSeries.IsWeierstrassDivisionAt.add, PowerSeries.add_weierstrassMod, PowerSeries.HasSubst.add, PowerSeries.IsWeierstrassDivisorAt.div_add, HasSubst.add, PowerSeries.HasSubst.hasEval, LaurentSeries.powerSeriesEquivSubring_coe_apply, HasEval.X, PowerSeries.invOneSubPow_eq_inv_one_sub_pow, PowerSeries.intValuation_X, substAlgHom_monomial, PowerSeries.isWeierstrassDivisionAt_iff, LaurentSeries.valuation_def, comp_subst, PowerSeries.IsWeierstrassDivisorAt.mk_mod'_eq_self, PowerSeries.substAlgHom_eq_aeval, coeff_subst_finite, HasSubst.hasEval, PowerSeries.WithPiTopology.multipliable_one_sub_X_pow, comp_substAlgHom, PowerSeries.coeff_mul_prod_one_sub_of_lt_order, Polynomial.IsDistinguishedAt.algEquivQuotient_apply, PowerSeries.add_weierstrassDiv, PowerSeries.hasSubst_iff_hasEval_of_discreteTopology, PowerSeries.HasEval.X, aeval_unique, coeff_mul_prod_one_sub_of_lt_weightedOrder
|
instCommSemiring 📖 | CompOp | 63 mathmath: PowerSeries.derivative_exp, PowerSeries.algebraMap_apply'', PowerSeries.instUniqueFactorizationMonoidOfIsPrincipalIdealRingOfIsDomain, PowerSeries.X_prime, PowerSeries.maximalIdeal_eq_span_X, PowerSeries.divXPowOrder_prod, PowerSeries.derivative_inv', le_order_prod, LaurentSeries.coe_algebraMap, ringKrullDim_succ_le_ringKrullDim_powerseries, le_weightedOrder_prod, WithPiTopology.multipliable_one_add_of_tendsto_order_atTop_nhds_top, PowerSeries.normUnit_X, Nat.Partition.hasProd_powerSeriesMk_card_countRestricted, PowerSeries.WithPiTopology.summable_prod_of_tendsto_order_atTop_nhds_top, PowerSeries.normalized_count_X_eq_of_coe, PowerSeries.prod_monomial, PowerSeries.instUniqueFactorizationMonoid, Nat.Partition.powerSeriesMk_card_restricted_eq_tprod, LaurentSeries.of_powerSeries_localization, PowerSeries.derivative_invOf, Nat.Partition.hasProd_powerSeriesMk_card_restricted, WithPiTopology.summable_prod_of_tendsto_weightedOrder_atTop_nhds_top, coeff_prod, substAlgHom_coe, algebraMap_apply'', Nat.Partition.powerSeriesMk_card_countRestricted_eq_tprod, PowerSeries.derivative_coe, PowerSeries.coeff_prod, PowerSeries.order_prod, HasSubst.smul, WithPiTopology.summable_prod_of_tendsto_order_atTop_nhds_top, Nat.Partition.multipliable_powerSeriesMk_card_restricted, PowerSeries.ker_coeff_eq_max_ideal, PowerSeries.coeff_derivative, PowerSeries.derivative_subst, monomial_one_eq, order_prod, monomial_eq, Nat.Partition.hasProd_genFun, PowerSeries.WithPiTopology.multipliable_one_add_of_tendsto_order_atTop_nhds_top, PowerSeries.derivative_C, PowerSeries.HasSubst.smul, LaurentSeries.instIsFractionRingPowerSeries, monomial_smul_const, Nat.Partition.multipliable_powerSeriesMk_card_countRestricted, PowerSeries.trunc_derivative, monomial_smul_eq, PowerSeries.le_order_prod, subst_coe, Nat.Partition.multipliable_genFun, PowerSeries.derivative_inv, PowerSeries.derivativeFun_mul, weightedOrder_prod, PowerSeries.derivative_X, monomial_eq', Nat.Partition.genFun_eq_tprod, PowerSeries.X_eq_normalizeX, prod_monomial, prod_smul_X_eq_smul_monomial_one, PowerSeries.derivative_pow, WithPiTopology.multipliable_one_add_of_tendsto_weightedOrder_atTop_nhds_top, PowerSeries.trunc_derivative'
|
instInhabited 📖 | CompOp | — |
instModule 📖 | CompOp | 365 mathmath: PowerSeries.coeff_mul_eq_coeff_trunc_mul_trunc₂, coeff_zero_eq_constantCoeff_apply, PowerSeries.coeff_toSubring, CuspFormClass.qExpansion_isBigO, hasSubst_def, PowerSeries.WithPiTopology.hasSum_iff_hasSum_coeff, WithPiTopology.tendsto_trunc_atTop, PowerSeries.hasSum_aeval, PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply, coeff_zero_eq_constantCoeff, PowerSeries.coeff_mul_one_sub_of_lt_order, coeff_zero, weightedOrder_monomial, eq_iff_frequently_trunc'_eq, PowerSeries.coeff_mul_of_lt_order, PowerSeries.IsRestricted.smul, PowerSeries.coeff_of_lt_order_toNat, PowerSeries.constantCoeff_subst, truncFinset_one, PowerSeries.WithPiTopology.continuous_coeff, trunc'_trunc', ModularFormClass.qExpansionFormalMultilinearSeries_apply_norm, PowerSeries.coeff_mul_C, coeff_mul_monomial, PowerSeries.coeff_rescale, PowerSeries.coeff_expand_mul, PowerSeries.catalanSeries_coeff, PowerSeries.coeff_X_mul_largeSchroderSeries, PowerSeries.coeff_trunc, PowerSeries.trunc_mul_trunc, PowerSeries.trunc_X_pow_self_mul, coeff_pow, PowerSeries.derivative_exp, PowerSeries.coeff_of_lt_order, constantCoeff_subst, trunc'_expand_trunc', PowerSeries.coeff_succ_mul_X, coeff_monomial_mul, PowerSeries.coeff_mul_mem_ideal_of_coeff_right_mem_ideal', coeff_X_pow, PowerSeries.gaussNorm_monomial, X_pow_eq, ext_trunc', PowerSeries.coeff_ne_zero_C, monomial_mem_nonzeroDivisors, PowerSeries.derivative_inv', coeff_mul_right_one_sub_of_lt_weightedOrder, Polynomial.coe_monomial, PowerSeries.aeval_eq_sum, PowerSeries.binomialSeries_coeff, monomial_mem_nonzeroDivisorsLeft, smul_eq_C_mul, trunc_C, PowerSeries.coeff_subst, PowerSeries.le_order_smul, coeff_eq_zero_of_constantCoeff_nilpotent, PowerSeries.coeff_coe, coeff_X, PowerSeries.eq_shift_mul_X_pow_add_trunc, PowerSeries.IsWeierstrassDivisorAt.coeff_seq_succ_sub_seq_mem, coeff_monomial_same, hasSum_aeval, coeff_truncFinset_of_mem, weightedOrder_monomial_of_ne_zero, PowerSeries.coeff_inv_aux, X_pow_dvd_iff, PowerSeries.degree_trunc_lt, coeff_mul_prod_one_sub_of_lt_order, PowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto, PowerSeries.coe_smul, coeff_index_single_X, PowerSeries.WithPiTopology.uniformContinuous_coeff, LinearTopology.mem_basis_iff, subst_monomial, PowerSeries.coeff_zero_one, coeff_of_lt_order, PowerSeries.coeff_X_mul_largeSchroderSeriesSeries_sq, trunc'_trunc'_pow, coeff_embDomain_rename, MvPolynomial.coe_monomial, X_def, ext_iff, trunc_one, PowerSeries.trunc_trunc_mul_trunc, PowerSeries.coeff_invOfUnit, WithPiTopology.continuous_coeff, PowerSeries.trunc_mul_C, PowerSeries.hasSum_of_monomials_self, coeff_trunc'_mul_trunc'_eq_coeff_mul, le_lexOrder_iff, monomial_mem_nonzeroDivisorsRight, PowerSeries.coeff_derivativeFun, coeff_index_single_self_X, WithPiTopology.as_tsum, WithPiTopology.uniformContinuous_coeff, monomial_zero_eq_C, coeff_inv, PowerSeries.eval₂_eq_tsum, PowerSeries.trunc_X_of, rename_monomial, PowerSeries.order_monomial, coeff_homogeneousComponent, PowerSeries.monomial_mul_monomial, weightedHomogeneousComponent_of_lt_weightedOrder_eq_zero, WithPiTopology.hasSum_iff_hasSum_coeff, PowerSeries.eq_X_mul_shift_add_const, coeff_subst, constantCoeff_smul, killCompl_monomial_embDomain, LaurentSeries.powerSeriesPart_coeff, PowerSeries.IsWeierstrassDivisorAt.mod'_mk_eq_mod, PowerSeries.coeff_invUnitsSub, PowerSeries.prod_monomial, PowerSeries.coeff_succ_C, PowerSeries.trunc_trunc_mul, truncFinset_C, HasSubst.coeff_zero, PowerSeries.IsRestricted.isRestricted_iff, coeff_one, truncFinset_map, PowerSeries.coeff_mul_mem_ideal_of_coeff_right_mem_ideal, PowerSeries.coeff_mk, coeff_truncFinset_mul_truncFinset_eq_coeff_mul, Polynomial.coe_smul, PowerSeries.sub_const_eq_X_mul_shift, PowerSeries.coeff_largeSchroderSeries, coeff_mul_right_one_sub_of_lt_order, coeff_expand_smul, le_weightedOrder_smul, truncFinset_monomial_eq_zero, HahnSeries.ofPowerSeries_apply_coeff, eval₂_eq_tsum, homogeneousComponent_of_lt_order_eq_zero, le_weightedOrder_subst, trunc'_expand, monomial_zero_eq_C_apply, PowerSeries.monomial_zero_eq_C, PowerSeries.monomial_pow, coeff_comp_monomial, PowerSeries.eq_X_pow_mul_shift_add_trunc, PowerSeries.trunc_trunc_of_le, ModularFormClass.qExpansion_coeff, trunc_map, PowerSeries.coeff_exp, PowerSeries.trunc_one_left, isHomogeneous_iff_eq_homogeneousComponent, MvPolynomial.coeff_coe, coeff_trunc', PowerSeries.sub_const_eq_shift_mul_X, LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero, coeff_zero_mul_X, coeff_inv_aux, coeff_weightedHomogeneousComponent, PowerSeries.derivative_invOf, PowerSeries.HasSubst.monomial', PowerSeries.IsWeierstrassDivisorAt.isUnit_shift, Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval, coeff_apply, PowerSeries.constantCoeff_divXPowOrder, PowerSeries.monomial_eq_mk, coeff_trunc, HahnSeries.toPowerSeriesAlg_symm_apply_coeff, eq_zero_iff_forall_coeff_eq_zero_and, PowerSeries.trunc_C, ModularFormClass.qExpansion_coeff_zero, coeff_prod, truncFinset_monomial, coeff_C_mul, PowerSeries.X_eq, weightedHomogeneousComponent_mul_of_le_weightedOrder, PowerSeries.coeff_comp_monomial, coeff_zero_one, PowerSeries.trunc_trunc_pow, PowerSeries.coeff_mul, HahnSeries.coeff_toPowerSeries, PowerSeries.IsWeierstrassDivisorAt.coeff_seq_mem, PowerSeries.coeff_smul, coeff_add_mul_monomial, monomial_pow, PowerSeries.coeff_monomial_same, coeff_zero_X_mul, map_monomial, PowerSeries.trunc_apply, le_order_smul, PowerSeries.coeff_mul_mem_ideal_of_coeff_left_mem_ideal', PowerSeries.coeff_monomial, coeff_zero_iff, PowerSeries.coeff_X, HahnSeries.coeff_toPowerSeries_symm, PowerSeries.IsWeierstrassDivisorAt.coeff_div, EisensteinSeries.E_qExpansion_coeff, coeff_mul_left_one_sub_of_lt_weightedOrder, weightedOrder_eq_nat, totalDegree_trunc', PowerSeries.as_tsum, expand_monomial, PowerSeries.derivative_coe, PowerSeries.coeff_zero_eq_constantCoeff_apply, HahnSeries.ofPowerSeriesAlg_apply_coeff, Polynomial.IsDistinguishedAt.algEquivQuotient_symm_apply, ModularFormClass.hasSum_qExpansion_of_abs_lt, PowerSeries.coeff_map, PowerSeries.constantCoeff_smul, coeff_rescale, WithPiTopology.hasSum_of_monomials_self, PowerSeries.coeff_one, PowerSeries.eq_shift_mul_X_add_const, PowerSeries.coeff_prod, PowerSeries.coeff_mul_X_pow', PowerSeries.coeff_zero_C, eq_zero_iff_forall_coeff_zero, PowerSeries.forall_coeff_eq_zero, PowerSeries.coeff_C, HahnSeries.coeff_toMvPowerSeries_symm, isWeightedHomogeneous_weightedHomogeneousComponent, PowerSeries.coeff_inv, coeff_expand_of_not_dvd, coeff_zero_C, coeff_monomial, X_dvd_iff, coeff_C, ModularFormClass.qExpansion_coeff_eq_circleIntegral, PowerSeries.coeff_expand_of_not_dvd, homogeneousComponent_mul_of_le_order, PowerSeries.coeff_subst_X_pow, PowerSeries.coeff_zero_eq_constantCoeff, LaurentSeries.coeff_zero_of_lt_intValuation, WithPiTopology.summable_iff_summable_coeff, instIsScalarTower, PowerSeries.X_pow_eq, coeff_invOfUnit, coeff_map, coeff_toSubring, PowerSeries.monomial_eq_C_mul_X_pow, coeff_mul_eq_coeff_trunc'_mul_trunc', killCompl_monomial_eq_zero, PowerSeries.le_gaussNorm, totalDegree_truncFinset, PowerSeries.coeff_divXPowOrder, PowerSeries.trunc_one, HahnSeries.SummableFamily.powerSeriesFamily_of_orderTop_pos, WithPiTopology.tendsto_trunc'_atTop, PowerSeries.ext_iff, PowerSeries.coeff_X_pow_self, PowerSeries.trunc_succ, coeff_smul, coeff_zero_X, ModularFormClass.qExpansion_isBigO, HahnSeries.coeff_toMvPowerSeries, PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal, order_monomial, PowerSeries.coeff_mul_eq_coeff_trunc_mul_trunc, substAlgHom_monomial, qExpansion_mul_coeff_zero, PowerSeries.trunc_coe_eq_self, coeff_truncFinset_eq_zero, PowerSeries.coeff_derivative, PowerSeries.coeff_subst_finite, PowerSeries.coeff_X_pow, isHomogeneous_homogeneousComponent, ModularFormClass.hasSum_qExpansion_of_norm_lt, coeff_killCompl, PowerSeries.expand_monomial, aeval_eq_sum, qExpansion_coeff_unique, PowerSeries.coeff_subst', PowerSeries.derivative_subst, monomial_zero_one, monomial_one_eq, PowerSeries.IsRestricted.monomial, PowerSeries.coeff_expand, PowerSeries.eval₂_trunc_eq_sum_range, PowerSeries.trunc_one_X, monomial_eq, PowerSeries.coeff_succ_X_mul, coeff_monomial_ne, PowerSeries.IsWeierstrassDivisorAt.mk_mod'_eq_self, PowerSeries.trunc_trunc, truncFinset_truncFinset, support_truncFinset_subset, coeff_truncFinset, coeff_subst_finite, order_eq_nat, IsWeightedHomogeneous.coeff_eq_zero, PowerSeries.coeff_C_mul, PowerSeries.X_pow_dvd_iff, coeff_rename_eq_zero, PowerSeries.coeff_mul_mem_ideal_of_coeff_left_mem_ideal, coeff_mul_left_one_sub_of_lt_order, PowerSeries.derivative_C, coeff_rename, PowerSeries.order_eq, monomial_mul_monomial, PowerSeries.coeff_zero_X_mul, EisensteinSeries.E_qExpansion_coeff_zero, PowerSeries.WithPiTopology.tendsto_trunc_atTop, PowerSeries.coeff_C_mul_X_pow, trunc'_one, trunc_C_mul, PowerSeries.coeff_X_pow_mul', WithPiTopology.tendsto_iff_coeff_tendsto, isWeightedHomogeneous_iff_eq_weightedHomogeneousComponent, PowerSeries.coeff_pow, PowerSeries.coeff_one_pow, monomial_smul_const, PowerSeries.coeff_mul_X_pow, trunc'_map, PowerSeries.smul_eq_C_mul, ModularFormClass.qExpansionFormalMultilinearSeries_coeff, PowerSeries.trunc_sub, hasSum_eval₂, PowerSeries.IsWeierstrassDivisorAt.seq_one, Nat.Partition.coeff_genFun, PowerSeries.trunc_derivativeFun, PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal', PowerSeries.coeff_subst_finite', PowerSeries.HasSubst.monomial, PowerSeries.trunc_map, PowerSeries.coeff_coe_trunc_of_lt, PowerSeries.trunc_zero', PowerSeries.coeff_mul_prod_one_sub_of_lt_order, HahnSeries.toPowerSeries_symm_apply_coeff, PowerSeries.trunc_derivative, monomial_smul_eq, LaurentSeries.coeff_coe_powerSeries, truncFinset_apply, order_monomial_of_ne_zero, ModularFormClass.hasSum_qExpansion, IsHomogeneous.coeff_eq_zero, qExpansion_coeff_isBigO_of_norm_isBigO, ModularFormClass.qExpansion_coeff_eq_intervalIntegral, PowerSeries.coeff_one_mul, coeff_eq_zero_of_lt_lexOrder, PowerSeries.monomial_zero_eq_C_apply, coeff_mul_of_add_lexOrder, Polynomial.coeff_coe, PowerSeries.derivative_inv, coeff_eq_zero_of_lt_weightedOrder, PowerSeries.natDegree_trunc_lt, PowerSeries.trunc_X, PowerSeries.derivative_X, monomial_eq', PowerSeries.IsWeierstrassDivisorAt.coeff_div_sub_seq_mem, PowerSeries.coeff_X_pow_mul, PowerSeries.coeff_zero_mul_X, coeff_mul_C, PowerSeries.order_monomial_of_ne_zero, PowerSeries.trunc_C_mul, coeff_mul, PowerSeries.WithPiTopology.summable_iff_summable_coeff, coeff_mul_prod_one_sub_of_lt_weightedOrder, coeff_add_monomial_mul, PowerSeries.hasSum_eval₂, trunc'_C, prod_monomial, prod_smul_X_eq_smul_monomial_one, PowerSeries.coeff_one_X, trunc'_C_mul, truncFinset_truncFinset_pow, commute_monomial, PowerSeries.derivative_pow, PowerSeries.order_eq_nat, PowerSeries.coeff_zero_X, PowerSeries.IsWeierstrassDivisionAt.coeff_f_sub_r_mem, PowerSeries.trunc_derivative'
|
instMul 📖 | CompOp | 199 mathmath: PowerSeries.coeff_mul_eq_coeff_trunc_mul_trunc₂, PowerSeries.coeff_mul_one_sub_of_lt_order, PowerSeries.coeff_mul_of_lt_order, PowerSeries.coeff_mul_C, coeff_mul_monomial, PowerSeries.weierstrassDistinguished_mul, PowerSeries.coeff_X_mul_largeSchroderSeries, PowerSeries.trunc_mul_trunc, PowerSeries.HasSubst.mul_right, PowerSeries.trunc_X_pow_self_mul, le_order_mul, PowerSeries.eq_mul_weierstrassDiv_add_weierstrassMod, PowerSeries.coeff_succ_mul_X, coeff_monomial_mul, PowerSeries.coeff_mul_mem_ideal_of_coeff_right_mem_ideal', X_pow_mul, PowerSeries.Inv_divided_by_X_pow_order_leftInv, commute_X_pow, PowerSeries.derivative_inv', PowerSeries.divXPowOrder_mul, PowerSeries.rescale_X, coeff_mul_right_one_sub_of_lt_weightedOrder, le_weightedOrder_mul, PowerSeries.inv_eq_iff_mul_eq_one, PowerSeries.order_mul_ge, smul_eq_C_mul, PowerSeries.subst_mul, Polynomial.bernoulli_generating_function, PowerSeries.eq_mul_inv_iff_mul_eq, eq_inv_iff_mul_eq_one, PowerSeries.eq_shift_mul_X_pow_add_trunc, bernoulliPowerSeries_mul_exp_sub_one, PowerSeries.binomialSeries_add, HahnSeries.toMvPowerSeries_symm_apply_coeff, DividedPowers.exp_add, coeff_mul_prod_one_sub_of_lt_order, weightedOrder_mul, subst_monomial, qExpansion_of_mul, PowerSeries.coeff_X_mul_largeSchroderSeriesSeries_sq, lexOrder_mul, commute_X, PowerSeries.mk_add_choose_mul_one_sub_pow_eq_one, PowerSeries.trunc_trunc_mul_trunc, PowerSeries.coe_mul, PowerSeries.trunc_mul_C, inv_eq_iff_mul_eq_one, PowerSeries.commute_X_pow, HahnSeries.SummableFamily.hsum_powerSeriesFamily_mul, coeff_trunc'_mul_trunc'_eq_coeff_mul, PowerSeries.IsWeierstrassDivisionAt.eq_mul_add, PowerSeries.IsRestricted.mul, PowerSeries.largeSchroderSeries_eq_one_add_X_mul_largeSchroderSeries_add_X_mul_largeSchroderSeries_sq, bernoulli'PowerSeries_mul_exp_sub_one, PowerSeries.mul_X_injective, PowerSeries.exp_mul_exp_neg_eq_one, mul_assoc, PowerSeries.monomial_mul_monomial, PowerSeries.weierstrassUnit_mul, PowerSeries.le_order_mul, PowerSeries.eq_X_mul_shift_add_const, PowerSeries.exp_mul_exp_eq_exp_add, subst_mul, inv_mul_cancel, PowerSeries.X_pow_mul, PowerSeries.trunc_trunc_mul, PowerSeries.coeff_mul_mem_ideal_of_coeff_right_mem_ideal, one_mul, coeff_truncFinset_mul_truncFinset_eq_coeff_mul, PowerSeries.sub_const_eq_X_mul_shift, coeff_mul_right_one_sub_of_lt_order, HasSubst.mul_right, invOfUnit_mul, PowerSeries.isWeierstrassFactorizationAt_iff, PowerSeries.mul_inv_cancel, PowerSeries.invUnitsSub_mul_sub, PowerSeries.eq_X_pow_mul_shift_add_trunc, IsWeightedHomogeneous.mul, PowerSeries.mul_inv_rev, PowerSeries.X_mul_inj, PowerSeries.mul_invOfUnit, PowerSeries.one_sub_pow_add_mul_invOneSubPow_val_eq_one_sub_pow, PowerSeries.sub_const_eq_shift_mul_X, coeff_zero_mul_X, weightedOrder_mul_ge, PowerSeries.WithPiTopology.one_sub_mul_tsum_pow_of_constantCoeff_eq_zero, WithPiTopology.one_sub_mul_tsum_pow_of_constantCoeff_eq_zero, PowerSeries.derivative_invOf, PowerSeries.one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val, Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval, X_mul, coeff_C_mul, PowerSeries.divXPowOrder_mul_divXPowOrder, PowerSeries.instNoZeroDivisors, weightedHomogeneousComponent_mul_of_le_weightedOrder, PowerSeries.coeff_mul, add_mul, HahnSeries.coeff_toPowerSeries, PowerSeries.IsWeierstrassDivisorAt.coeff_seq_mem, mul_zero, coeff_add_mul_monomial, PowerSeries.X_mul, WithPiTopology.tsum_pow_mul_one_sub_of_constantCoeff_eq_zero, coeff_zero_X_mul, PowerSeries.coeff_mul_mem_ideal_of_coeff_left_mem_ideal', PowerSeries.X_pow_mul_injective, HahnSeries.coeff_toPowerSeries_symm, coeff_mul_left_one_sub_of_lt_weightedOrder, LaurentSeries.powerSeriesRingEquiv_coe_apply, LaurentSeries.powerSeriesEquivSubring_apply, PowerSeries.IsWeierstrassFactorizationAt.eq_mul, zero_mul, PowerSeries.eq_shift_mul_X_add_const, PowerSeries.coeff_mul_X_pow', Polynomial.coe_mul, HahnSeries.coeff_toMvPowerSeries_symm, PowerSeries.HasSubst.mul_left, PowerSeries.WithPiTopology.tsum_pow_mul_one_sub_of_constantCoeff_eq_zero, homogeneousComponent_mul_of_le_order, LaurentSeries.powerSeriesEquivSubring_coe_apply, DividedPowers.exp_add', PowerSeries.monomial_eq_C_mul_X_pow, PowerSeries.mul_X_pow_injective, PowerSeries.eq_inv_iff_mul_eq_one, coeff_mul_eq_coeff_trunc'_mul_trunc', order_mul_ge, mul_inv_cancel, HahnSeries.coeff_toMvPowerSeries, qExpansion_mul, PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal, PowerSeries.coeff_mul_eq_coeff_trunc_mul_trunc, substAlgHom_monomial, mul_invOfUnit, PowerSeries.catalanSeries_sq_mul_X_add_one, PowerSeries.isWeierstrassDivisionAt_iff, IsHomogeneous.mul, PowerSeries.derivative_subst, HahnSeries.ofPowerSeries_apply, PowerSeries.X_pow_order_mul_divXPowOrder, HahnSeries.toMvPowerSeries_apply, eq_mul_inv_iff_mul_eq, PowerSeries.coeff_succ_X_mul, PowerSeries.eq_weierstrassDistinguished_mul_weierstrassUnit, instNoZeroDivisors, PowerSeries.coeff_C_mul, PowerSeries.coeff_mul_mem_ideal_of_coeff_left_mem_ideal, coeff_mul_left_one_sub_of_lt_order, PowerSeries.X_pow_mul_inj, PowerSeries.IsWeierstrassFactorizationAt.mul, order_mul, ModularForm.qExpansion_mul, monomial_mul_monomial, PowerSeries.coeff_zero_X_mul, PowerSeries.invUnitsSub_mul_X, mul_add, PowerSeries.coeff_C_mul_X_pow, trunc_C_mul, PowerSeries.coeff_X_pow_mul', mul_inv_rev, PowerSeries.order_mul, HahnSeries.toPowerSeries_apply, PowerSeries.coeff_mul_X_pow, PowerSeries.smul_eq_C_mul, PowerSeries.IsWeierstrassDivisorAt.seq_one, PowerSeries.Inv_divided_by_X_pow_order_rightInv, PowerSeries.heval_mul, HahnSeries.SummableFamily.support_powerSeriesFamily_subset, PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal', LaurentSeries.X_order_mul_powerSeriesPart, PowerSeries.mul_X_pow_inj, le_lexOrder_mul, PowerSeries.coeff_mul_prod_one_sub_of_lt_order, PowerSeries.mk_one_mul_one_sub_eq_one, HahnSeries.toPowerSeries_symm_apply_coeff, monomial_smul_eq, PowerSeries.coeff_one_mul, coeff_mul_of_add_lexOrder, PowerSeries.mul_X_inj, PowerSeries.derivative_inv, PowerSeries.derivativeFun_mul, PowerSeries.X_mul_injective, monomial_eq', PowerSeries.coeff_X_pow_mul, PowerSeries.coeff_zero_mul_X, coeff_mul_C, HasSubst.mul_left, PowerSeries.commute_X, MvPolynomial.coe_mul, PowerSeries.trunc_C_mul, coeff_mul, coeff_mul_prod_one_sub_of_lt_weightedOrder, PowerSeries.inv_mul_cancel, lexOrder_mul_ge, coeff_add_monomial_mul, PowerSeries.invOfUnit_mul, mul_one, trunc'_C_mul, commute_monomial, PowerSeries.derivative_pow
|
instOne 📖 | CompOp | 80 mathmath: Polynomial.coe_eq_one_iff, PowerSeries.coeff_mul_one_sub_of_lt_order, truncFinset_one, PowerSeries.invOneSubPow_inv_eq_one_sub_pow, PowerSeries.Inv_divided_by_X_pow_order_leftInv, Polynomial.coe_one, coeff_mul_right_one_sub_of_lt_weightedOrder, PowerSeries.inv_eq_iff_mul_eq_one, Polynomial.bernoulli_generating_function, MvPolynomial.coe_one, eq_inv_iff_mul_eq_one, bernoulliPowerSeries_mul_exp_sub_one, coeff_mul_prod_one_sub_of_lt_order, WithPiTopology.multipliable_one_add_of_tendsto_order_atTop_nhds_top, MvPolynomial.coe_eq_one_iff, PowerSeries.binomialSeries_zero, PowerSeries.coeff_zero_one, PowerSeries.mk_add_choose_mul_one_sub_pow_eq_one, trunc_one, PowerSeries.divXPowOrder_one, inv_eq_iff_mul_eq_one, PowerSeries.largeSchroderSeries_eq_one_add_X_mul_largeSchroderSeries_add_X_mul_largeSchroderSeries_sq, bernoulli'PowerSeries_mul_exp_sub_one, PowerSeries.exp_mul_exp_neg_eq_one, PowerSeries.constantCoeff_one, qExpansion_one, inv_mul_cancel, Nat.Partition.powerSeriesMk_card_restricted_eq_tprod, PowerSeries.invOneSubPow_inv_zero_eq_one, coeff_one, one_mul, coeff_mul_right_one_sub_of_lt_order, invOfUnit_mul, PowerSeries.mul_inv_cancel, PowerSeries.invUnitsSub_mul_sub, PowerSeries.mul_invOfUnit, PowerSeries.one_sub_pow_add_mul_invOneSubPow_val_eq_one_sub_pow, PowerSeries.WithPiTopology.one_sub_mul_tsum_pow_of_constantCoeff_eq_zero, WithPiTopology.one_sub_mul_tsum_pow_of_constantCoeff_eq_zero, PowerSeries.derivative_invOf, PowerSeries.one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val, Nat.Partition.hasProd_powerSeriesMk_card_restricted, coeff_zero_one, PowerSeries.derivativeFun_one, WithPiTopology.tsum_pow_mul_one_sub_of_constantCoeff_eq_zero, coeff_mul_left_one_sub_of_lt_weightedOrder, constantCoeff_one, PowerSeries.coeff_one, PowerSeries.order_one, PowerSeries.WithPiTopology.tsum_pow_mul_one_sub_of_constantCoeff_eq_zero, PowerSeries.eq_inv_iff_mul_eq_one, Nat.Partition.multipliable_powerSeriesMk_card_restricted, PowerSeries.IsRestricted.one, PowerSeries.trunc_one, PowerSeries.invOneSubPow_eq_inv_one_sub_pow, mul_inv_cancel, mul_invOfUnit, PowerSeries.catalanSeries_sq_mul_X_add_one, monomial_zero_one, PowerSeries.coe_one, Nat.Partition.hasProd_genFun, PowerSeries.WithPiTopology.multipliable_one_add_of_tendsto_order_atTop_nhds_top, coeff_mul_left_one_sub_of_lt_order, PowerSeries.invUnitsSub_mul_X, trunc'_one, PowerSeries.binomialSeries_nat, PowerSeries.Inv_divided_by_X_pow_order_rightInv, PowerSeries.WithPiTopology.multipliable_one_sub_X_pow, PowerSeries.coeff_mul_prod_one_sub_of_lt_order, PowerSeries.mk_one_mul_one_sub_eq_one, Nat.Partition.multipliable_genFun, PowerSeries.divXPowOrder_X, weightedOrder_one, PowerSeries.derivative_X, Nat.Partition.genFun_eq_tprod, coeff_mul_prod_one_sub_of_lt_weightedOrder, PowerSeries.inv_mul_cancel, PowerSeries.invOfUnit_mul, mul_one, WithPiTopology.multipliable_one_add_of_tendsto_weightedOrder_atTop_nhds_top
|
instRing 📖 | CompOp | 16 mathmath: PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_apply, PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply, WithPiTopology.instIsTopologicalRing, LinearTopology.basis_le_iff, PowerSeries.IsRestricted.add, LinearTopology.mem_basis_iff, LinearTopology.instIsLinearTopologyMulOpposite, PowerSeries.IsWeierstrassDivisorAt.mod'_mk_eq_mod, LinearTopology.instIsLinearTopologyOfMulOpposite, Polynomial.IsDistinguishedAt.algEquivQuotient_symm_apply, PowerSeries.WithPiTopology.instIsTopologicalRing, PowerSeries.IsWeierstrassDivisorAt.mk_mod'_eq_self, PowerSeries.binomialSeries_nat, Polynomial.IsDistinguishedAt.algEquivQuotient_apply, LinearTopology.hasBasis_nhds_zero, LinearTopology.basis_le
|
instSemiring 📖 | CompOp | 561 mathmath: coeff_zero_eq_constantCoeff_apply, PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_apply, hasSubst_def, PowerSeries.hasSum_aeval, PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply, MvPolynomial.coe_C, Polynomial.eval₂_C_X_eq_coe, PowerSeries.rescale_eq_subst, coeff_zero_eq_constantCoeff, PowerSeries.constantCoeff_expand, PowerSeries.constantCoeff_subst, PowerSeries.coeff_mul_C, PowerSeries.heval_C, PowerSeries.coeff_rescale, subst_pow, support_expand, PowerSeries.invOneSubPow_zero, qExpansionRingHom_apply, PowerSeries.coeff_expand_mul, PowerSeries.spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_X_mem, PowerSeries.expand_subst, PowerSeries.expand_apply, rescaleUnit, PowerSeries.trunc_X_pow_self_mul, coeff_pow, PowerSeries.invOneSubPow_inv_eq_one_sub_pow, LaurentSeries.LaurentSeriesRingEquiv_def, constantCoeff_subst, PowerSeries.algebraMap_apply'', PowerSeries.spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_isPrime, PowerSeries.order_expand, PowerSeries.eq_divided_by_X_pow_order_Iff_Unit, coeff_X_pow, X_pow_mul, PowerSeries.Unit_of_divided_by_X_pow_order_zero, commute_X_pow, PowerSeries.degree_weierstrassMod_lt, X_pow_eq, mapAlgHom_apply, HahnSeries.ofPowerSeries_X_pow, eval₂Hom_eq_extend, WithPiTopology.isTopologicallyNilpotent_iff_constantCoeff_isNilpotent, subst_C, HasSubst.map, map_algebraMap_eq_subst_X, PowerSeries.coeff_ne_zero_C, PowerSeries.HasSubst.smul', substAlgHom_X, min_lexOrder_le, continuous_aeval, PowerSeries.mapAlgHom_apply, monomial_mem_nonzeroDivisors, PowerSeries.derivative_inv', coe_substAlgHom, PowerSeries.instIsDomain, PowerSeries.rescale_X, Nat.Partition.tendsto_order_genFun_term_atTop_nhds_top, rename_map, PowerSeries.coe_add, PowerSeries.catalanSeries_constantCoeff, PowerSeries.coeff_heval, PowerSeries.isUnit_exp, PowerSeries.aeval_eq_sum, LaurentSeries.ofPowerSeries_powerSeriesPart, IsWeightedHomogeneous.add, LaurentSeries.single_order_mul_powerSeriesPart, isUnit_iff_constantCoeff, PowerSeries.subst_rescale_of_degree_eq_one, monomial_mem_nonzeroDivisorsLeft, expand_mul, smul_eq_C_mul, Polynomial.coe_C, trunc_C, PowerSeries.coeff_subst, Polynomial.bernoulli_generating_function, Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_map, PowerSeries.isUnit_divided_by_X_pow_order, rescale_mul, PowerSeries.map_cos, coeff_eq_zero_of_constantCoeff_nilpotent, PowerSeries.coeff_coe, killCompl_comp_rename, PowerSeries.constantCoeff_X, PowerSeries.eq_shift_mul_X_pow_add_trunc, LaurentSeries.coe_algebraMap, expand_substAlgHom, PowerSeries.support_expand_subset, RatFunc.coe_coe, PowerSeries.isUnit_iff_constantCoeff, PowerSeries.subst_pow, substAlgHom_eq_aeval, PowerSeries.WithPiTopology.continuous_constantCoeff, hasSum_aeval, PowerSeries.derivativeFun_smul, PowerSeries.support_expand, HahnSeries.toMvPowerSeries_symm_apply_coeff, X_pow_dvd_iff, PowerSeries.IsWeierstrassFactorization.isWeierstrassDivision, PowerSeries.smul_weierstrassDiv, PowerSeries.coe_smul, comp_aeval, WithPiTopology.multipliable_one_add_of_tendsto_order_atTop_nhds_top, subst_monomial, le_weightedOrder_map, PowerSeries.coeff_X_mul_largeSchroderSeriesSeries_sq, trunc'_trunc'_pow, mem_nonZeroDivisors_of_constantCoeff, coeff_embDomain_rename, PowerSeries.map_constantCoeff_le_self_of_X_mem, PowerSeries.IsWeierstrassDivision.isUnit_of_map_ne_zero, renameEquiv_symm, map_subst, WithPiTopology.instContinuousSMul, LaurentSeries.val_le_one_iff_eq_coe, PowerSeries.constantCoeff_invUnitsSub, PowerSeries.mk_add_choose_mul_one_sub_pow_eq_one, coe_eval₂Hom, PowerSeries.rescale_rescale, PowerSeries.coe_mul, PowerSeries.trunc_mul_C, PowerSeries.IsWeierstrassDivisionAt.degree_lt, PowerSeries.rescale_zero_apply, PowerSeries.commute_X_pow, PowerSeries.substAlgHom_X, expand_one_apply, PowerSeries.IsWeierstrassFactorizationAt.natDegree_eq_toNat_order_map_of_ne_top, PowerSeries.heval_apply, LinearTopology.isTopologicallyNilpotent_iff_constantCoeff, one_le_order_iff_constCoeff_eq_zero, Nat.Partition.hasProd_powerSeriesMk_card_countRestricted, PowerSeries.coe_sub, PowerSeries.mk_one_pow_eq_mk_choose_add, constantCoeff_invOfUnit, monomial_mem_nonzeroDivisorsRight, PowerSeries.expand_one_apply, rename_rename, constantCoeff_inv, le_weightedOrder_pow, PowerSeries.rescale_zero, PowerSeries.le_order_map, PowerSeries.aeval_unique, PowerSeries.rescale_mk, PowerSeries.HasSubst.X_pow, PowerSeries.constantCoeff_surj, PowerSeries.largeSchroderSeries_eq_one_add_X_mul_largeSchroderSeries_add_X_mul_largeSchroderSeries_sq, min_weightedOrder_le_add, constantCoeff_C, PowerSeries.substAlgHom_comp_substAlgHom, monomial_zero_eq_C, coeff_inv, constantCoeff_comp_C, PowerSeries.exp_mul_exp_neg_eq_one, HasSubst.comp, rename_C, PowerSeries.constantCoeff_one, PowerSeries.map_sin, PowerSeries.derivativeFun_C, rename_monomial, PowerSeries.constantCoeff_invOfUnit, Polynomial.constantCoeff_coe, PowerSeries.rescale_algebraMap_map, PowerSeries.HasSubst.smul_X', PowerSeries.expand_smul, PowerSeries.C_injective, rescaleAlgHom_one, c_eq_algebraMap, rename_id, Nat.Partition.summable_genFun_term, PowerSeries.eq_X_mul_shift_add_const, coeff_subst, expand_eq_expand, substAlgHom_comp_substAlgHom_apply, instIsLocalRing, constantCoeff_smul, PowerSeries.constantCoeff_comp_C, killCompl_monomial_embDomain, HasSubst.const_coeff, PowerSeries.exp_mul_exp_eq_exp_add, PowerSeries.IsWeierstrassDivisorAt.mod'_mk_eq_mod, PowerSeries.evalNegHom_X, rescaleAlgHom_mul, PowerSeries.X_pow_mul, PowerSeries.coeff_succ_C, LinearTopology.isTopologicallyNilpotent_of_constantCoeff, truncFinset_C, PowerSeries.IsWeierstrassFactorization.natDegree_eq_toNat_order_map, expand_one, constantCoeff_zero, PowerSeries.WithPiTopology.instIsTopologicalSemiring, Nat.Partition.powerSeriesMk_card_restricted_eq_tprod, PowerSeries.invOneSubPow_inv_zero_eq_one, PowerSeries.smul_weierstrassMod, PowerSeries.exp_pow_sum, PowerSeries.one_le_order_iff_constCoeff_eq_zero, truncFinset_map, C_inv, HahnSeries.SummableFamily.powerSeriesFamily_hsum_zero, WithPiTopology.summable_pow_of_constantCoeff_eq_zero, PowerSeries.sub_const_eq_X_mul_shift, PowerSeries.constantCoeff_C, Polynomial.coe_add, coeff_expand_smul, PowerSeries.constantCoeff_inv, rename_id_apply, aeval_coe, PowerSeries.isWeierstrassFactorizationAt_iff, HahnSeries.ofPowerSeries_apply_coeff, LaurentSeries.of_powerSeries_localization, trunc'_expand, PowerSeries.invUnitsSub_mul_sub, PowerSeries.X_irreducible, monomial_zero_eq_C_apply, PowerSeries.monomial_zero_eq_C, PowerSeries.monomial_pow, PowerSeries.instNontrivialSubalgebra, comp_subst_apply, PowerSeries.eq_X_pow_mul_shift_add_trunc, PowerSeries.constantCoeff_subst_eq_zero, rename_coe, PowerSeries.WithPiTopology.isTopologicallyNilpotent_iff_constantCoeff_isNilpotent, PowerSeries.map_eq_zero, HahnSeries.ofPowerSeries_X, trunc_map, PowerSeries.isUnit_weierstrassUnit, PowerSeries.rescale_map, PowerSeries.one_sub_pow_add_mul_invOneSubPow_val_eq_one_sub_pow, PowerSeries.spanFinrank_eq_spanFinrank_map_constantCoeff_of_X_notMem_of_fg_of_isPrime, LaurentSeries.coe_X_compare, PowerSeries.not_isField, PowerSeries.sub_const_eq_shift_mul_X, LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero, PowerSeries.IsWeierstrassFactorizationAt.isUnit, PowerSeries.coe_divXPowOrderHom, PowerSeries.WithPiTopology.one_sub_mul_tsum_pow_of_constantCoeff_eq_zero, WithPiTopology.one_sub_mul_tsum_pow_of_constantCoeff_eq_zero, PowerSeries.le_order_pow_of_constantCoeff_eq_zero, PowerSeries.derivative_invOf, PowerSeries.one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val, PowerSeries.coe_zero, PowerSeries.IsWeierstrassDivisorAt.isUnit_shift, PowerSeries.map_X, Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval, instNontrivialSubalgebraOfNonempty, PowerSeries.map_comp, PowerSeries.constantCoeff_divXPowOrder, HahnSeries.toPowerSeriesAlg_apply, PowerSeries.inv_eq_zero, HahnSeries.toPowerSeriesAlg_symm_apply_coeff, LaurentSeries.exists_powerSeries_of_memIntegers, expand_subst, map_toSubring, PowerSeries.trunc_C, Nat.Partition.hasProd_powerSeriesMk_card_restricted, killCompl_rename_app, HasSubst.X_pow, PowerSeries.WithPiTopology.continuous_C, PowerSeries.coe_C, rename_inj, map_eq_zero, MvPolynomial.coe_add, PowerSeries.coe_neg, coeff_C_mul, PowerSeries.min_order_le_order_add, constantCoeff_toSubring, PowerSeries.gaussNorm_C, substAlgHom_coe, PowerSeries.map_subst, algebraMap_apply'', PowerSeries.subst_C, rescale_homogeneous_eq_smul, PowerSeries.expand_C, killCompl_map, PowerSeries.map_algebraMap_eq_subst_X, rescale_zero, PowerSeries.trunc_trunc_pow, PowerSeries.constantCoeff_largeSchroderSeries, PowerSeries.C_eq_algebraMap, HahnSeries.coeff_toPowerSeries, MvPolynomial.coe_pow, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, monomial_pow, expand_comp_substAlgHom, map_map, PowerSeries.subst_coe, PowerSeries.invOfUnit_eq, PowerSeries.map_surjective, WithPiTopology.tsum_pow_mul_one_sub_of_constantCoeff_eq_zero, rescale_rescale, PowerSeries.map_invUnitsSub, map_monomial, MvPolynomial.coeToMvPowerSeries.algHom_apply, constantCoeff_subst_eq_zero, rename_comp_rename, PowerSeries.le_order_pow, isUnit_constantCoeff, PowerSeries.constantCoeff_divXPowOrder_eq_zero_iff, PowerSeries.X_pow_mul_injective, PowerSeries.expand_mul, mem_nonZeroDivisorsLeft_of_constantCoeff, PowerSeries.IsWeierstrassDivisorAt.mod_smul, HahnSeries.coeff_toPowerSeries_symm, PowerSeries.constantCoeff_zero, PowerSeries.expand_mul_eq_comp, map_id, PowerSeries.invOneSubPow_add, PowerSeries.fg_iff_of_isPrime, Polynomial.coeToPowerSeries.algHom_apply, PowerSeries.order_pow, LaurentSeries.powerSeriesRingEquiv_coe_apply, expand_monomial, Nat.Partition.powerSeriesMk_card_countRestricted_eq_tprod, PowerSeries.Unit_of_divided_by_X_pow_order_nonzero, PowerSeries.coeff_zero_eq_constantCoeff_apply, inv_eq_zero, order_expand, HahnSeries.ofPowerSeriesAlg_apply_coeff, LaurentSeries.powerSeriesEquivSubring_apply, map_iterateFrobenius_expand, Polynomial.IsDistinguishedAt.algEquivQuotient_symm_apply, MvPolynomial.coe_smul, PowerSeries.coeff_map, PowerSeries.eval₂_C, PowerSeries.constantCoeff_smul, PowerSeries.heval_X, PowerSeries.comp_aeval, coeff_rescale, constantCoeff_rename, constantCoeff_one, PowerSeries.exist_eq_span_eq_ncard_of_X_notMem, PowerSeries.constantCoeff_mk, PowerSeries.eq_shift_mul_X_add_const, PowerSeries.coeff_mul_X_pow', PowerSeries.coeff_zero_C, Polynomial.algebraMap_hahnSeries_apply, algebraMap_apply', PowerSeries.coeff_C, HahnSeries.coeff_toMvPowerSeries_symm, order_ne_zero_iff_constCoeff_eq_zero, renameEquiv_refl, PowerSeries.coeff_inv, coeff_expand_of_not_dvd, PowerSeries.rescale_injective, Polynomial.coeToPowerSeries.ringHom_apply, PowerSeries.map_expand, rescaleAlgHom_apply, coeff_zero_C, X_dvd_iff, coeff_C, PowerSeries.WithPiTopology.tsum_pow_mul_one_sub_of_constantCoeff_eq_zero, PowerSeries.coeff_expand_of_not_dvd, LaurentSeries.powerSeriesEquivSubring_coe_apply, map.isLocalHom, PowerSeries.coeff_subst_X_pow, PowerSeries.coe_eval₂Hom, PowerSeries.coeff_zero_eq_constantCoeff, constantCoeff_map, rescale_eq_subst, PowerSeries.coe_X, coe_aeval, killCompl_X_eq_zero, weightedOrder_add_of_weightedOrder_ne, constantCoeff_X, rename_injective, HasSubst.smul_X, map_frobenius_expand, PowerSeries.invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos, PowerSeries.exp_pow_eq_rescale_exp, PowerSeries.X_pow_eq, coeff_map, PowerSeries.monomial_eq_C_mul_X_pow, PowerSeries.mul_X_pow_injective, Nat.Partition.summable_genFun_term', Nat.Partition.multipliable_powerSeriesMk_card_restricted, expand_X, map_expand, PowerSeries.divXPowOrder_pow, PowerSeries.HasSubst.comp, killCompl_monomial_eq_zero, MvPolynomial.coeToMvPowerSeries.ringHom_apply, PowerSeries.X_pow_order_dvd, PowerSeries.ker_coeff_eq_max_ideal, renameEquiv_apply, PowerSeries.algebraMap_eq, constantCoeff_expand, PowerSeries.coeff_X_pow_self, PowerSeries.continuous_aeval, PowerSeries.map_C, PowerSeries.heval_unit, PowerSeries.invOneSubPow_eq_inv_one_sub_pow, HahnSeries.coeff_toMvPowerSeries, PowerSeries.IsWeierstrassDivision.isWeierstrassFactorization, PowerSeries.IsWeierstrassFactorization.degree_eq_coe_lift_order_map, substAlgHom_monomial, PowerSeries.rescale_neg_one_X, PowerSeries.constantCoeff_exp, PowerSeries.coe_orderHom, algebraMap_apply, PowerSeries.catalanSeries_sq_mul_X_add_one, PowerSeries.coeff_subst_finite, PowerSeries.coeff_X_pow, PowerSeries.IsWeierstrassFactorizationAt.degree_eq_coe_lift_order_map_of_ne_top, coeff_killCompl, PowerSeries.expand_monomial, aeval_eq_sum, PowerSeries.isWeierstrassDivisionAt_iff, PowerSeries.coeff_subst', PowerSeries.constantCoeff_toSubring, PowerSeries.C_inv, WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_isNilpotent, IsNilpotent_subst, monomial_one_eq, PowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_isNilpotent, order_add_of_order_ne, PowerSeries.coeff_expand, PowerSeries.algebraMap_apply, PowerSeries.coe_aeval, PowerSeries.derivativeFun_add, HahnSeries.ofPowerSeries_apply, comp_subst, PowerSeries.expand_one, monomial_eq, PowerSeries.X_pow_order_mul_divXPowOrder, PowerSeries.map_exp, HahnSeries.toMvPowerSeries_apply, PowerSeries.coe_one, PowerSeries.IsWeierstrassDivisorAt.mk_mod'_eq_self, PowerSeries.span_X_isPrime, PowerSeries.invOneSubPow_val_one_eq_invUnitSub_one, PowerSeries.inv_eq_inv_aux, PowerSeries.coe_rescaleAlgHom, invOfUnit_eq, WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_zero, PowerSeries.aeval_coe, Nat.Partition.hasProd_genFun, coeff_subst_finite, PowerSeries.coeff_heval_zero, PowerSeries.order_ne_zero_iff_constCoeff_eq_zero, X_mem_nonzeroDivisors, WithPiTopology.instIsTopologicalSemiring, HahnSeries.ofPowerSeries_injective, PowerSeries.IsWeierstrassFactorizationAt.smul, HasSubst.pow, PowerSeries.substAlgHom_coe, PowerSeries.WithPiTopology.multipliable_one_add_of_tendsto_order_atTop_nhds_top, PowerSeries.coeff_C_mul, PowerSeries.X_pow_dvd_iff, coeff_rename_eq_zero, mem_nonZeroDivisorsRight_of_constantCoeff, PowerSeries.rescale_eq, PowerSeries.derivative_C, PowerSeries.X_pow_mul_inj, PowerSeries.IsWeierstrassDivisorAt.div_smul, coeff_rename, subst_smul, support_expand_subset, PowerSeries.expand_X, PowerSeries.X_dvd_iff, PowerSeries.order_add_of_order_ne, PowerSeries.invUnitsSub_mul_X, rescale_one, PowerSeries.subst_smul, eval₂_C, PowerSeries.rescale_one, PowerSeries.IsWeierstrassDivisionAt.smul, PowerSeries.coeff_C_mul_X_pow, trunc_C_mul, map_X, killCompl_X, PowerSeries.order_eq_emultiplicity_X, PowerSeries.coeff_X_pow_mul', rename_X, PowerSeries.binomialSeries_nat, map_C, PowerSeries.algebraMap_apply', HahnSeries.ofPowerSeries_C, PowerSeries.coe_pow, PowerSeries.substAlgHom_comp_substAlgHom_apply, PowerSeries.weierstrassUnit_smul, killCompl_C, PowerSeries.coeff_pow, LaurentSeries.mem_integers_of_powerSeries, PowerSeries.binomialSeries_constantCoeff, PowerSeries.coeff_one_pow, HahnSeries.toPowerSeries_apply, monomial_smul_const, PowerSeries.coeff_mul_X_pow, trunc'_map, PowerSeries.smul_eq_C_mul, rescale_zero_apply, expand_mul_eq_comp, PowerSeries.IsWeierstrassDivisorAt.seq_one, Nat.Partition.multipliable_powerSeriesMk_card_countRestricted, PowerSeries.map_id, le_order_pow, PowerSeries.WithPiTopology.multipliable_one_sub_X_pow, PowerSeries.order_X_pow, PowerSeries.heval_mul, comp_substAlgHom, PowerSeries.rescale_neg_one_invOneSubPow, HahnSeries.algebraMap_apply', PowerSeries.coeff_subst_finite', PowerSeries.trunc_map, PowerSeries.smul_inv, qExpansion_of_pow, LaurentSeries.X_order_mul_powerSeriesPart, PowerSeries.mul_X_pow_inj, qExpansion_smul, PowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_zero, PowerSeries.HasSubst.smul_X, Polynomial.polynomial_map_coe, min_order_le_add, HahnSeries.toPowerSeries_symm_apply_coeff, monomial_smul_eq, LaurentSeries.coeff_coe_powerSeries, Polynomial.IsDistinguishedAt.algEquivQuotient_apply, PowerSeries.coeff_one_mul, PowerSeries.constantCoeff_subst_X_pow, PowerSeries.monomial_zero_eq_C_apply, PowerSeries.map_toSubring, smul_inv, substAlgHom_apply, Nat.Partition.multipliable_genFun, WithPiTopology.continuous_constantCoeff, substAlgHom_comp_substAlgHom, Polynomial.coe_pow, PowerSeries.IsRestricted.C, HahnSeries.SummableFamily.powerSeriesFamily_smul, PowerSeries.derivative_inv, PowerSeries.isUnit_constantCoeff, aeval_unique, HasSubst.expand, PowerSeries.derivativeFun_mul, PowerSeries.coe_substAlgHom, PowerSeries.rescale_mul, PowerSeries.WithPiTopology.summable_pow_of_constantCoeff_eq_zero, monomial_eq', PowerSeries.map.isLocalHom, PowerSeries.invOneSubPow_val_succ_eq_mk_add_choose, PowerSeries.coeff_X_pow_mul, PowerSeries.map_injective, coeff_mul_C, IsHomogeneous.add, PowerSeries.weierstrassDistinguished_smul, le_order_pow_of_constantCoeff_eq_zero, map_comp, LaurentSeries.valuation_X_pow, Nat.Partition.genFun_eq_tprod, Polynomial.IsDistinguishedAt.coe_natDegree_eq_order_map, renameEquiv_trans, PowerSeries.trunc_C_mul, PowerSeries.instIsNoetherianRing, expand_C, trunc'_C, prod_smul_X_eq_smul_monomial_one, trunc'_C_mul, truncFinset_truncFinset_pow, WithPiTopology.continuous_C, PowerSeries.eq_span_insert_X_of_X_mem_of_span_eq, PowerSeries.derivative_pow, WithPiTopology.multipliable_one_add_of_tendsto_weightedOrder_atTop_nhds_top, le_order_map
|
instZero 📖 | CompOp | 77 mathmath: zero_inv, coeff_zero, qExpansion_eq_zero_iff, PowerSeries.zero_weierstrassDiv, PowerSeries.IsWeierstrassDivisorAt.div_coe_eq_zero, PowerSeries.zero_weierstrassMod, PowerSeries.HasSubst.zero, PowerSeries.Unit_of_divided_by_X_pow_order_zero, Polynomial.coe_eq_zero_iff, Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_map, PowerSeries.gaussNorm_zero, MvPolynomial.coe_eq_zero_iff, LinearTopology.isTopologicallyNilpotent_iff_constantCoeff, MvPolynomial.coe_zero, PowerSeries.derivativeFun_C, weightedHomogeneousComponent_of_lt_weightedOrder_eq_zero, PowerSeries.IsWeierstrassDivision.eq_zero, PowerSeries.weierstrassDiv_zero, constantCoeff_zero, PowerSeries.X_inv, PowerSeries.order_zero, PowerSeries.weierstrassDiv_zero_right, homogeneousComponent_of_lt_order_eq_zero, PowerSeries.HasSubst.zero', PowerSeries.WithPiTopology.isTopologicallyNilpotent_iff_constantCoeff_isNilpotent, PowerSeries.map_eq_zero, lexOrder_zero, PowerSeries.coe_zero, PowerSeries.zero_inv, PowerSeries.inv_eq_zero, eq_zero_iff_forall_coeff_eq_zero_and, PowerSeries.weierstrassMod_zero_left, map_eq_zero, PowerSeries.instNoZeroDivisors, PowerSeries.derivativeFun_one, mul_zero, order_eq_top_iff, PowerSeries.constantCoeff_divXPowOrder_eq_zero_iff, coeff_zero_iff, PowerSeries.constantCoeff_zero, inv_eq_zero, zero_mul, eq_zero_iff_forall_coeff_zero, PowerSeries.forall_coeff_eq_zero, lexOrder_eq_top_iff_eq_zero, killCompl_X_eq_zero, PowerSeries.IsWeierstrassDivisorAt.mod_zero, PowerSeries.gaussNorm_eq_zero_iff, HasSubst.zero, X_inv, killCompl_monomial_eq_zero, PowerSeries.IsWeierstrassFactorization.degree_eq_coe_lift_order_map, PowerSeries.IsWeierstrassFactorizationAt.degree_eq_coe_lift_order_map_of_ne_top, PowerSeries.IsWeierstrassDivisorAt.eq_zero_of_mul_eq, PowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_isNilpotent, Polynomial.coe_zero, weightedOrder_zero, PowerSeries.order_eq_top, instNoZeroDivisors, WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_zero, PowerSeries.IsWeierstrassDivisorAt.div_zero, WithPiTopology.variables_tendsto_zero, PowerSeries.derivative_C, PowerSeries.weierstrassMod_zero_right, PowerSeries.weierstrassMod_zero, qExpansion_zero, order_zero, weightedOrder_eq_top_iff, PowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_zero, PowerSeries.weierstrassDiv_zero_left, LaurentSeries.powerSeriesPart_zero, PowerSeries.IsWeierstrassDivisorAt.seq_zero, LinearTopology.hasBasis_nhds_zero, PowerSeries.isWeierstrassDivisionAt_zero, PowerSeries.divXPowOrder_zero, PowerSeries.IsRestricted.zero, LaurentSeries.powerSeriesPart_eq_zero
|
map 📖 | CompOp | 29 mathmath: mapAlgHom_apply, HasSubst.map, map_algebraMap_eq_subst_X, rename_map, le_weightedOrder_map, map_subst, truncFinset_map, trunc_map, map_toSubring, map_eq_zero, PowerSeries.map_subst, algebraMap_apply'', killCompl_map, map_map, map_monomial, MvPolynomial.coeToMvPowerSeries.algHom_apply, map_id, map_iterateFrobenius_expand, algebraMap_apply', map.isLocalHom, constantCoeff_map, map_frobenius_expand, coeff_map, map_expand, map_X, map_C, trunc'_map, map_comp, le_order_map
|
mapAlgHom 📖 | CompOp | 1 mathmath: mapAlgHom_apply
|
monomial 📖 | CompOp | 44 mathmath: weightedOrder_monomial, coeff_mul_monomial, coeff_monomial_mul, X_pow_eq, monomial_mem_nonzeroDivisors, monomial_mem_nonzeroDivisorsLeft, coeff_monomial_same, weightedOrder_monomial_of_ne_zero, subst_monomial, MvPolynomial.coe_monomial, X_def, monomial_def, monomial_mem_nonzeroDivisorsRight, WithPiTopology.as_tsum, monomial_zero_eq_C, rename_monomial, killCompl_monomial_embDomain, truncFinset_monomial_eq_zero, monomial_zero_eq_C_apply, coeff_comp_monomial, truncFinset_monomial, coeff_add_mul_monomial, monomial_pow, map_monomial, expand_monomial, WithPiTopology.hasSum_of_monomials_self, coeff_monomial, killCompl_monomial_eq_zero, order_monomial, substAlgHom_monomial, monomial_zero_one, monomial_one_eq, monomial_eq, coeff_monomial_ne, monomial_mul_monomial, monomial_smul_const, PowerSeries.HasSubst.monomial, monomial_smul_eq, order_monomial_of_ne_zero, monomial_eq', coeff_add_monomial_mul, prod_monomial, prod_smul_X_eq_smul_monomial_one, commute_monomial
|
toSubring 📖 | CompOp | 5 mathmath: map_toSubring, constantCoeff_toSubring, order_toSubring, coeff_toSubring, weightedOrder_toSubring
|