| Name | Category | Theorems |
|---|
C 📖 | CompOp | 25 mathmath: MvPolynomial.coe_C, smul_eq_C_mul, trunc_C, constantCoeff_C, monomial_zero_eq_C, constantCoeff_comp_C, c_eq_algebraMap, C_inv, monomial_zero_eq_C_apply, coeff_C_mul, rescale_zero, coeff_zero_C, coeff_C, algebraMap_apply, eval₂_C, trunc_C_mul, map_C, rescale_zero_apply, monomial_smul_eq, monomial_eq', coeff_mul_C, expand_C, trunc'_C, trunc'_C_mul, WithPiTopology.continuous_C
|
X 📖 | CompOp | 42 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, 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, 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 | 90 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, X_pow_dvd_iff, coeff_mul_prod_one_sub_of_lt_order, coeff_index_single_X, LinearTopology.mem_basis_iff, coeff_of_lt_order, ext_iff, WithPiTopology.continuous_coeff, 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_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_truncFun', 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, coeff_truncFun, 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_mul_eq_coeff_trunc'_mul_trunc', coeff_smul, coeff_zero_X, HahnSeries.coeff_toMvPowerSeries, PowerSeries.coeff_subst_finite, aeval_eq_sum, coeff_monomial_ne, coeff_subst_finite, order_eq_nat, IsWeightedHomogeneous.coeff_eq_zero, coeff_mul_left_one_sub_of_lt_order, WithPiTopology.tendsto_iff_coeff_tendsto, hasSum_eval₂, 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 | 29 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, constantCoeff_toSubring, rescale_zero, isUnit_constantCoeff, inv_eq_zero, constantCoeff_one, order_ne_zero_iff_constCoeff_eq_zero, constantCoeff_map, constantCoeff_X, constantCoeff_expand, invOfUnit_eq, rescale_zero_apply, WithPiTopology.continuous_constantCoeff
|
instAddCommGroup 📖 | CompOp | 4 mathmath: LinearTopology.instIsLinearTopologyMulOpposite, LinearTopology.instIsLinearTopologyOfMulOpposite, weightedOrder_neg, order_neg
|
instAddCommMonoid 📖 | CompOp | 138 mathmath: coeff_zero_eq_constantCoeff_apply, hasSubst_def, coeff_zero_eq_constantCoeff, coeff_zero, weightedOrder_monomial, coeff_mul_monomial, coeff_pow, constantCoeff_subst, coeff_monomial_mul, coeff_X_pow, X_pow_eq, WithPiTopology.summable_of_tendsto_order_atTop_nhds_top, monomial_mem_nonzeroDivisors, coeff_mul_right_one_sub_of_lt_weightedOrder, monomial_mem_nonzeroDivisorsLeft, smul_eq_C_mul, PowerSeries.coeff_subst, coeff_eq_zero_of_constantCoeff_nilpotent, coeff_X, coeff_monomial_same, hasSum_aeval, weightedOrder_monomial_of_ne_zero, X_pow_dvd_iff, coeff_mul_prod_one_sub_of_lt_order, coeff_index_single_X, LinearTopology.mem_basis_iff, subst_monomial, coeff_of_lt_order, MvPolynomial.coe_monomial, X_def, ext_iff, WithPiTopology.continuous_coeff, le_lexOrder_iff, monomial_mem_nonzeroDivisorsRight, coeff_index_single_self_X, WithPiTopology.as_tsum, WithPiTopology.uniformContinuous_coeff, monomial_zero_eq_C, coeff_inv, coeff_homogeneousComponent, weightedHomogeneousComponent_of_lt_weightedOrder_eq_zero, WithPiTopology.hasSum_iff_hasSum_coeff, coeff_subst, constantCoeff_smul, HasSubst.coeff_zero, coeff_one, WithPiTopology.summable_pow_of_constantCoeff_eq_zero, coeff_mul_right_one_sub_of_lt_order, coeff_expand_smul, le_weightedOrder_smul, eval₂_eq_tsum, homogeneousComponent_of_lt_order_eq_zero, le_weightedOrder_subst, monomial_zero_eq_C_apply, coeff_comp_monomial, isHomogeneous_iff_eq_homogeneousComponent, MvPolynomial.coeff_coe, coeff_trunc', coeff_zero_mul_X, coeff_inv_aux, WithPiTopology.one_sub_mul_tsum_pow_of_constantCoeff_eq_zero, coeff_weightedHomogeneousComponent, coeff_apply, coeff_trunc, eq_zero_iff_forall_coeff_eq_zero_and, coeff_truncFun', WithPiTopology.summable_prod_of_tendsto_weightedOrder_atTop_nhds_top, coeff_prod, coeff_C_mul, weightedHomogeneousComponent_mul_of_le_weightedOrder, coeff_zero_one, add_mul, coeff_add_mul_monomial, monomial_pow, WithPiTopology.tsum_pow_mul_one_sub_of_constantCoeff_eq_zero, coeff_zero_X_mul, map_monomial, le_order_smul, coeff_zero_iff, coeff_mul_left_one_sub_of_lt_weightedOrder, weightedOrder_eq_nat, expand_monomial, coeff_rescale, WithPiTopology.hasSum_of_monomials_self, eq_zero_iff_forall_coeff_zero, coeff_truncFun, HahnSeries.coeff_toMvPowerSeries_symm, isWeightedHomogeneous_weightedHomogeneousComponent, coeff_expand_of_not_dvd, coeff_zero_C, coeff_monomial, X_dvd_iff, coeff_C, homogeneousComponent_mul_of_le_order, WithPiTopology.summable_prod_of_tendsto_order_atTop_nhds_top, WithPiTopology.summable_iff_summable_coeff, instIsScalarTower, coeff_invOfUnit, coeff_map, coeff_mul_eq_coeff_trunc'_mul_trunc', coeff_smul, coeff_zero_X, HahnSeries.coeff_toMvPowerSeries, order_monomial, substAlgHom_monomial, PowerSeries.coeff_subst_finite, isHomogeneous_homogeneousComponent, aeval_eq_sum, monomial_zero_one, monomial_one_eq, monomial_eq, coeff_monomial_ne, coeff_subst_finite, order_eq_nat, IsWeightedHomogeneous.coeff_eq_zero, coeff_mul_left_one_sub_of_lt_order, monomial_mul_monomial, mul_add, WithPiTopology.tendsto_iff_coeff_tendsto, isWeightedHomogeneous_iff_eq_weightedHomogeneousComponent, monomial_smul_const, hasSum_eval₂, PowerSeries.HasSubst.monomial, monomial_smul_eq, order_monomial_of_ne_zero, IsHomogeneous.coeff_eq_zero, coeff_eq_zero_of_lt_lexOrder, coeff_mul_of_add_lexOrder, coeff_eq_zero_of_lt_weightedOrder, monomial_eq', coeff_mul_C, coeff_mul, coeff_mul_prod_one_sub_of_lt_weightedOrder, WithPiTopology.summable_of_tendsto_weightedOrder_atTop_nhds_top, coeff_add_monomial_mul, prod_monomial, prod_smul_X_eq_smul_monomial_one, commute_monomial
|
instAddGroup 📖 | CompOp | 9 mathmath: coeff_mul_right_one_sub_of_lt_weightedOrder, coeff_mul_prod_one_sub_of_lt_order, coeff_mul_right_one_sub_of_lt_order, WithPiTopology.instIsUniformAddGroup, WithPiTopology.one_sub_mul_tsum_pow_of_constantCoeff_eq_zero, WithPiTopology.tsum_pow_mul_one_sub_of_constantCoeff_eq_zero, coeff_mul_left_one_sub_of_lt_weightedOrder, coeff_mul_left_one_sub_of_lt_order, coeff_mul_prod_one_sub_of_lt_weightedOrder
|
instAddMonoid 📖 | CompOp | 26 mathmath: WithPiTopology.tendsto_trunc_atTop, eq_iff_frequently_trunc'_eq, trunc'_trunc', trunc'_expand_trunc', ext_trunc', smul_eq_C_mul, trunc_C, trunc'_trunc'_pow, trunc_one, constantCoeff_smul, le_weightedOrder_smul, trunc'_expand, trunc_map, coeff_trunc', coeff_trunc, le_order_smul, totalDegree_trunc', instIsScalarTower, coeff_mul_eq_coeff_trunc'_mul_trunc', WithPiTopology.tendsto_trunc'_atTop, coeff_smul, trunc'_one, trunc_C_mul, trunc'_map, trunc'_C, trunc'_C_mul
|
instAddMonoidWithOne 📖 | CompOp | 1 mathmath: PowerSeries.derivative_pow
|
instAlgebra 📖 | CompOp | 71 mathmath: support_expand, subst_eq_eval₂, PowerSeries.expand_subst, mapAlgHom_apply, PowerSeries.HasSubst.smul', substAlgHom_X, continuous_aeval, coe_substAlgHom, expand_mul, expand_substAlgHom, substAlgHom_eq_aeval, hasSum_aeval, comp_aeval, subst_monomial, WithPiTopology.instContinuousSMul, PowerSeries.substAlgHom_X, expand_one_apply, PowerSeries.substAlgHom_comp_substAlgHom, HasSubst.comp, rescaleAlgHom_one, c_eq_algebraMap, expand_eq_expand, substAlgHom_comp_substAlgHom_apply, rescaleAlgHom_mul, expand_one, coeff_expand_smul, aeval_coe, trunc'_expand, instNontrivialSubalgebraOfNonempty, expand_subst, substAlgHom_coe, rescale_homogeneous_eq_smul, expand_comp_substAlgHom, PowerSeries.subst_coe, MvPolynomial.coeToMvPowerSeries.algHom_apply, expand_monomial, order_expand, map_iterateFrobenius_expand, MvPolynomial.coe_smul, coeff_expand_of_not_dvd, rescaleAlgHom_apply, rescale_eq_subst, coe_aeval, HasSubst.smul_X, map_frobenius_expand, expand_X, map_expand, PowerSeries.HasSubst.comp, constantCoeff_expand, substAlgHom_monomial, algebraMap_apply, aeval_eq_sum, IsNilpotent_subst, monomial_eq, PowerSeries.substAlgHom_eq_aeval, PowerSeries.substAlgHom_coe, subst_smul, support_expand_subset, PowerSeries.subst_smul, PowerSeries.substAlgHom_comp_substAlgHom_apply, monomial_smul_const, expand_mul_eq_comp, PowerSeries.HasSubst.smul_X, subst_coe, smul_inv, substAlgHom_apply, substAlgHom_comp_substAlgHom, HasSubst.expand, PowerSeries.coe_substAlgHom, expand_C, prod_smul_X_eq_smul_monomial_one
|
instCommRing 📖 | CompOp | 23 mathmath: subst_eq_eval₂, constantCoeff_subst, subst_add, substAlgHom_eq_aeval, coeff_mul_prod_one_sub_of_lt_order, subst_monomial, coeff_subst, comp_subst_apply, hasSubst_iff_hasEval_of_discreteTopology, PowerSeries.subst_add, PowerSeries.HasSubst.add, HasSubst.add, PowerSeries.HasSubst.hasEval, HasEval.X, substAlgHom_monomial, comp_subst, PowerSeries.substAlgHom_eq_aeval, coeff_subst_finite, HasSubst.hasEval, comp_substAlgHom, PowerSeries.hasSubst_iff_hasEval_of_discreteTopology, aeval_unique, coeff_mul_prod_one_sub_of_lt_weightedOrder
|
instCommSemiring 📖 | CompOp | 21 mathmath: le_order_prod, le_weightedOrder_prod, WithPiTopology.multipliable_one_add_of_tendsto_order_atTop_nhds_top, WithPiTopology.summable_prod_of_tendsto_weightedOrder_atTop_nhds_top, coeff_prod, substAlgHom_coe, algebraMap_apply'', HasSubst.smul, WithPiTopology.summable_prod_of_tendsto_order_atTop_nhds_top, monomial_one_eq, order_prod, monomial_eq, PowerSeries.HasSubst.smul, monomial_smul_const, monomial_smul_eq, subst_coe, weightedOrder_prod, monomial_eq', prod_monomial, prod_smul_X_eq_smul_monomial_one, WithPiTopology.multipliable_one_add_of_tendsto_weightedOrder_atTop_nhds_top
|
instInhabited 📖 | CompOp | — |
instModule 📖 | CompOp | 129 mathmath: coeff_zero_eq_constantCoeff_apply, hasSubst_def, coeff_zero_eq_constantCoeff, coeff_zero, weightedOrder_monomial, coeff_mul_monomial, coeff_pow, constantCoeff_subst, coeff_monomial_mul, coeff_X_pow, X_pow_eq, monomial_mem_nonzeroDivisors, coeff_mul_right_one_sub_of_lt_weightedOrder, monomial_mem_nonzeroDivisorsLeft, smul_eq_C_mul, PowerSeries.coeff_subst, coeff_eq_zero_of_constantCoeff_nilpotent, coeff_X, coeff_monomial_same, hasSum_aeval, weightedOrder_monomial_of_ne_zero, X_pow_dvd_iff, coeff_mul_prod_one_sub_of_lt_order, coeff_index_single_X, LinearTopology.mem_basis_iff, subst_monomial, coeff_of_lt_order, MvPolynomial.coe_monomial, X_def, ext_iff, WithPiTopology.continuous_coeff, le_lexOrder_iff, monomial_mem_nonzeroDivisorsRight, coeff_index_single_self_X, WithPiTopology.as_tsum, WithPiTopology.uniformContinuous_coeff, monomial_zero_eq_C, coeff_inv, coeff_homogeneousComponent, weightedHomogeneousComponent_of_lt_weightedOrder_eq_zero, WithPiTopology.hasSum_iff_hasSum_coeff, coeff_subst, constantCoeff_smul, HasSubst.coeff_zero, coeff_one, coeff_mul_right_one_sub_of_lt_order, coeff_expand_smul, le_weightedOrder_smul, eval₂_eq_tsum, homogeneousComponent_of_lt_order_eq_zero, le_weightedOrder_subst, monomial_zero_eq_C_apply, coeff_comp_monomial, isHomogeneous_iff_eq_homogeneousComponent, 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_truncFun', coeff_prod, coeff_C_mul, weightedHomogeneousComponent_mul_of_le_weightedOrder, coeff_zero_one, coeff_add_mul_monomial, monomial_pow, coeff_zero_X_mul, map_monomial, le_order_smul, coeff_zero_iff, coeff_mul_left_one_sub_of_lt_weightedOrder, weightedOrder_eq_nat, expand_monomial, coeff_rescale, WithPiTopology.hasSum_of_monomials_self, eq_zero_iff_forall_coeff_zero, coeff_truncFun, HahnSeries.coeff_toMvPowerSeries_symm, isWeightedHomogeneous_weightedHomogeneousComponent, coeff_expand_of_not_dvd, coeff_zero_C, coeff_monomial, X_dvd_iff, coeff_C, homogeneousComponent_mul_of_le_order, WithPiTopology.summable_iff_summable_coeff, instIsScalarTower, coeff_invOfUnit, coeff_map, coeff_mul_eq_coeff_trunc'_mul_trunc', coeff_smul, coeff_zero_X, HahnSeries.coeff_toMvPowerSeries, order_monomial, substAlgHom_monomial, PowerSeries.coeff_subst_finite, isHomogeneous_homogeneousComponent, aeval_eq_sum, monomial_zero_one, monomial_one_eq, monomial_eq, coeff_monomial_ne, coeff_subst_finite, order_eq_nat, IsWeightedHomogeneous.coeff_eq_zero, coeff_mul_left_one_sub_of_lt_order, monomial_mul_monomial, WithPiTopology.tendsto_iff_coeff_tendsto, isWeightedHomogeneous_iff_eq_weightedHomogeneousComponent, monomial_smul_const, hasSum_eval₂, PowerSeries.HasSubst.monomial, monomial_smul_eq, order_monomial_of_ne_zero, IsHomogeneous.coeff_eq_zero, coeff_eq_zero_of_lt_lexOrder, coeff_mul_of_add_lexOrder, coeff_eq_zero_of_lt_weightedOrder, monomial_eq', coeff_mul_C, coeff_mul, coeff_mul_prod_one_sub_of_lt_weightedOrder, coeff_add_monomial_mul, prod_monomial, prod_smul_X_eq_smul_monomial_one, commute_monomial
|
instMul 📖 | CompOp | 197 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, 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, 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 | 79 mathmath: Polynomial.coe_eq_one_iff, PowerSeries.coeff_mul_one_sub_of_lt_order, 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 | 7 mathmath: WithPiTopology.instIsTopologicalRing, LinearTopology.basis_le_iff, LinearTopology.mem_basis_iff, LinearTopology.instIsLinearTopologyMulOpposite, LinearTopology.instIsLinearTopologyOfMulOpposite, LinearTopology.hasBasis_nhds_zero, LinearTopology.basis_le
|
instSemiring 📖 | CompOp | 178 mathmath: coeff_zero_eq_constantCoeff_apply, hasSubst_def, MvPolynomial.coe_C, coeff_zero_eq_constantCoeff, PowerSeries.constantCoeff_subst, subst_pow, support_expand, PowerSeries.expand_subst, rescaleUnit, coeff_pow, constantCoeff_subst, coeff_X_pow, X_pow_mul, commute_X_pow, X_pow_eq, mapAlgHom_apply, eval₂Hom_eq_extend, WithPiTopology.isTopologicallyNilpotent_iff_constantCoeff_isNilpotent, map_algebraMap_eq_subst_X, PowerSeries.HasSubst.smul', substAlgHom_X, min_lexOrder_le, continuous_aeval, monomial_mem_nonzeroDivisors, coe_substAlgHom, IsWeightedHomogeneous.add, isUnit_iff_constantCoeff, monomial_mem_nonzeroDivisorsLeft, expand_mul, smul_eq_C_mul, trunc_C, PowerSeries.coeff_subst, rescale_mul, expand_substAlgHom, PowerSeries.subst_pow, substAlgHom_eq_aeval, hasSum_aeval, HahnSeries.toMvPowerSeries_symm_apply_coeff, X_pow_dvd_iff, comp_aeval, WithPiTopology.multipliable_one_add_of_tendsto_order_atTop_nhds_top, subst_monomial, le_weightedOrder_map, trunc'_trunc'_pow, map_subst, WithPiTopology.instContinuousSMul, coe_eval₂Hom, PowerSeries.substAlgHom_X, expand_one_apply, LinearTopology.isTopologicallyNilpotent_iff_constantCoeff, one_le_order_iff_constCoeff_eq_zero, constantCoeff_invOfUnit, monomial_mem_nonzeroDivisorsRight, constantCoeff_inv, le_weightedOrder_pow, min_weightedOrder_le_add, constantCoeff_C, PowerSeries.substAlgHom_comp_substAlgHom, monomial_zero_eq_C, coeff_inv, constantCoeff_comp_C, HasSubst.comp, rescaleAlgHom_one, c_eq_algebraMap, coeff_subst, expand_eq_expand, substAlgHom_comp_substAlgHom_apply, instIsLocalRing, constantCoeff_smul, HasSubst.const_coeff, rescaleAlgHom_mul, expand_one, constantCoeff_zero, C_inv, coeff_expand_smul, aeval_coe, trunc'_expand, monomial_zero_eq_C_apply, trunc_map, instNontrivialSubalgebraOfNonempty, expand_subst, map_toSubring, HasSubst.X_pow, map_eq_zero, MvPolynomial.coe_add, coeff_C_mul, constantCoeff_toSubring, substAlgHom_coe, PowerSeries.map_subst, algebraMap_apply'', rescale_homogeneous_eq_smul, rescale_zero, MvPolynomial.coe_pow, monomial_pow, expand_comp_substAlgHom, map_map, PowerSeries.subst_coe, rescale_rescale, map_monomial, MvPolynomial.coeToMvPowerSeries.algHom_apply, map_id, expand_monomial, inv_eq_zero, order_expand, map_iterateFrobenius_expand, MvPolynomial.coe_smul, coeff_rescale, constantCoeff_one, algebraMap_apply', HahnSeries.coeff_toMvPowerSeries_symm, order_ne_zero_iff_constCoeff_eq_zero, coeff_expand_of_not_dvd, rescaleAlgHom_apply, coeff_zero_C, X_dvd_iff, coeff_C, map.isLocalHom, constantCoeff_map, rescale_eq_subst, coe_aeval, weightedOrder_add_of_weightedOrder_ne, constantCoeff_X, HasSubst.smul_X, map_frobenius_expand, coeff_map, expand_X, map_expand, PowerSeries.HasSubst.comp, MvPolynomial.coeToMvPowerSeries.ringHom_apply, constantCoeff_expand, HahnSeries.coeff_toMvPowerSeries, substAlgHom_monomial, algebraMap_apply, PowerSeries.coeff_subst_finite, aeval_eq_sum, monomial_one_eq, order_add_of_order_ne, monomial_eq, HahnSeries.toMvPowerSeries_apply, invOfUnit_eq, coeff_subst_finite, X_mem_nonzeroDivisors, WithPiTopology.instIsTopologicalSemiring, PowerSeries.substAlgHom_coe, subst_smul, support_expand_subset, rescale_one, PowerSeries.subst_smul, eval₂_C, trunc_C_mul, map_X, map_C, PowerSeries.substAlgHom_comp_substAlgHom_apply, monomial_smul_const, trunc'_map, rescale_zero_apply, expand_mul_eq_comp, le_order_pow, PowerSeries.HasSubst.smul_X, min_order_le_add, monomial_smul_eq, smul_inv, substAlgHom_apply, WithPiTopology.continuous_constantCoeff, substAlgHom_comp_substAlgHom, HasSubst.expand, PowerSeries.coe_substAlgHom, monomial_eq', coeff_mul_C, IsHomogeneous.add, map_comp, expand_C, trunc'_C, prod_smul_X_eq_smul_monomial_one, trunc'_C_mul, WithPiTopology.continuous_C, WithPiTopology.multipliable_one_add_of_tendsto_weightedOrder_atTop_nhds_top, le_order_map
|
instZero 📖 | CompOp | 28 mathmath: zero_inv, coeff_zero, PowerSeries.HasSubst.zero, MvPolynomial.coe_eq_zero_iff, LinearTopology.isTopologicallyNilpotent_iff_constantCoeff, MvPolynomial.coe_zero, weightedHomogeneousComponent_of_lt_weightedOrder_eq_zero, constantCoeff_zero, homogeneousComponent_of_lt_order_eq_zero, lexOrder_zero, eq_zero_iff_forall_coeff_eq_zero_and, map_eq_zero, mul_zero, order_eq_top_iff, coeff_zero_iff, inv_eq_zero, zero_mul, eq_zero_iff_forall_coeff_zero, lexOrder_eq_top_iff_eq_zero, HasSubst.zero, X_inv, weightedOrder_zero, instNoZeroDivisors, WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_zero, WithPiTopology.variables_tendsto_zero, order_zero, weightedOrder_eq_top_iff, LinearTopology.hasBasis_nhds_zero
|
map 📖 | CompOp | 25 mathmath: mapAlgHom_apply, map_algebraMap_eq_subst_X, le_weightedOrder_map, map_subst, trunc_map, map_toSubring, map_eq_zero, PowerSeries.map_subst, algebraMap_apply'', 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 | 39 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, monomial_zero_eq_C_apply, coeff_comp_monomial, coeff_add_mul_monomial, monomial_pow, map_monomial, expand_monomial, WithPiTopology.hasSum_of_monomials_self, coeff_monomial, 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
|