| Name | Category | Theorems |
|---|
coeff 📖 | CompOp | 118 mathmath: coeff_fun_eq_zero_iff, HahnModule.coeff_single_smul_vadd, coeff_single_mul_add, VertexOperator.of_coeff_apply_coeff, LaurentSeries.valuation_le_iff_coeff_lt_eq_zero, HVertexOperator.coeff_isPWOsupport, single.addMonoidHom_apply_coeff, PowerSeries.coeff_heval, coeff_single_same, coeff_mul, SummableFamily.coeff_hsum_mul, embDomain_notin_range, PowerSeries.coeff_coe, LaurentSeries.Cauchy.coeff_tendsto, coeff_mul_left', toMvPowerSeries_symm_apply_coeff, SummableFamily.co_support_zero, HahnEmbedding.Partial.coeff_eq_of_mem, coeff_smul, embDomain_notin_image_support, coeff_untop_eq_leadingCoeff, coeff_sub, coeff_single_zero_mul, coeff_injective, coeff_smul', LaurentSeries.derivative_iterate_coeff, coeff_sum, embDomain_mk_coeff, SummableFamily.smul_support_subset_prod, SummableFamily.finite_co_support_prod_smul, SummableFamily.smul_support_finite, LaurentSeries.powerSeriesPart_coeff, coeff_neg, coeff_truncLT, embDomain_coeff, SummableFamily.coeff_support, leadingCoeff_of_ne, HahnModule.coeff_smul_order_add_order, isPWO_support', coeff_order_of_eq_add_single, ofPowerSeries_apply_coeff, embDomainAlgHom_apply_coeff, coeff_mul_order_add_order, coeff_ofSuppBddBelow, LaurentSeries.hasseDeriv_comp_coeff, coeff_single_of_ne, HahnEmbedding.Seed.coeff_baseEmbedding, leadingCoeff_eq, coeff_truncLT_of_le, toPowerSeriesAlg_apply, toPowerSeriesAlg_symm_apply_coeff, coeff_ofFinsupp, ofSuppBddBelow_coeff, HahnModule.ext_iff, SummableFamily.coeff_smul, LaurentSeries.hasseDeriv_coeff, coeff_inj, HahnModule.coeff_smul, coeff_toPowerSeries, coeff_order_eq_zero, HahnModule.coeff_single_zero_smul, SummableFamily.finite_co_support_prod_mul, coeff_one, coeff_single, coeff_toPowerSeries_symm, HahnEmbedding.Partial.coeff_eq_zero_of_mem, coeff_zero', ofPowerSeriesAlg_apply_coeff, coeff_add, coeff_sub', coeff_toMvPowerSeries_symm, SummableFamily.pow_finite_co_support, LaurentSeries.coeff_zero_of_lt_valuation, SummableFamily.coeff_hsum, coeff_neg', SummableFamily.sum_vAddAntidiagonal_eq, coeff_mul_right', lt_iff, coeff_toMvPowerSeries, ext_iff, coeff_mul_single, coeff_truncLT_of_lt, HVertexOperator.compHahnSeries_coeff, le_order_iff_forall, coeff_zero, SummableFamily.hsum_smulFamily, LaurentSeries.valuation_le_iff_coeff_lt_log_eq_zero, SummableFamily.finite_co_support', LaurentSeries.uniformContinuous_coeff, toMvPowerSeries_apply, SummableFamily.coeff_apply, coeff_toOrderTopSubOnePos_pow, addOppositeEquiv_symm_apply_coeff, HVertexOperator.coeff_apply_apply, HahnModule.coeff_smul_left, HahnModule.coeff_smul_right, PowerSeries.coeff_heval_zero, coeff_mul_single_add, HahnEmbedding.Partial.evalCoeff_eq, coeff_mul_single_zero, map_coeff, addOppositeEquiv_apply, coeff_eq_zero_of_lt_order, toPowerSeries_apply, coeff_nsmul, LaurentSeries.eq_coeff_of_valuation_sub_lt, SummableFamily.coeff_hsum_eq_sum, SummableFamily.coeff_def, coeff.addMonoidHom_apply, toPowerSeries_symm_apply_coeff, LaurentSeries.coeff_coe_powerSeries, coeff_add', coeff_eq_zero_of_lt_orderTop, leadingCoeff_of_ne_zero, le_orderTop_iff_forall, SummableFamily.finite_co_support, coeff_single_mul, coeff_ofFinsuppLinearMap
|
embDomain 📖 | CompOp | 17 mathmath: embDomain_smul, embDomainLinearMap_apply, embDomain_notin_range, embDomainRingHom_apply, embDomain_notin_image_support, embDomain_one, embDomain_mk_coeff, embDomainOrderEmbedding_apply, embDomain_injective, embDomain_single, embDomain_coeff, embDomain_add, embDomain_mul, ofPowerSeries_apply, embDomain_zero, support_embDomain_subset, orderTop_embDomain
|
instInhabited 📖 | CompOp | — |
instZero 📖 | CompOp | 136 mathmath: HahnEmbedding.Seed.baseEmbedding_pos, SummableFamily.zero_apply, instNoZeroDivisorsFinsuppNat, untop_orderTop_of_ne_zero, orderTop_single_le, map_single, SummableFamily.embDomain_apply, coeff_fun_eq_zero_iff, cardSupp_single_of_ne, HahnModule.coeff_single_smul_vadd, SummableFamily.powers_zero, coeff_single_mul_add, orderTop_sub_pos, single_zero_natCast, single_zero_ofScientific, cardSupp_single_le, ofPowerSeries_X_pow, LaurentSeries.valuation_single_zpow, single_pow, SummableFamily.embDomain_notin_range, coeff_single_same, ofSuppBddBelow_zero, single_zero_nnratCast, SummableFamily.binomialFamily_apply_of_orderTop_nonpos, LaurentSeries.ofPowerSeries_powerSeriesPart, LaurentSeries.single_order_mul_powerSeriesPart, single_zero_intCast, RatFunc.coe_X, single_mul_single, single_zero_mul_eq_smul, SummableFamily.powerSeriesFamily_of_not_orderTop_pos, cardSupp_truncLT_le, instIsCancelMulZeroOfIsCancelAdd, single_sub, SummableFamily.co_support_zero, single_eq_zero_iff, order_single_mul_of_isRegular, coeff_single_zero_mul, coe_truncLTLinearMap, SummableFamily.single_toFun, SummableFamily.embDomain_succ_smul_powers, orderTop_eq_top_iff, truncLT_add, support_truncLT, embDomain_single, lt_orderTop_single, orderTop_of_ne, coeff_truncLT, ofSuppBddBelow_eq_zero, HVertexOperator.compHahnSeries_smul, leadingCoeff_of_ne, SummableFamily.powerSeriesFamily_hsum_zero, leadingCoeff_pos_iff, instNoZeroDivisors, unit_aux, orderTop_eq_top, ofPowerSeries_X, coeff_single_of_ne, SummableFamily.hsum_ofFinsupp, cardSupp_mul_single_le, C_zero, HVertexOperator.compHahnSeries_add, PowerSeries.coe_zero, coeff_truncLT_of_le, cardSupp_single_mul_le, support_eq_empty_iff, coeff_ofFinsupp, map_zero, single_neg, single_injective, cardSupp_zero, orderTop_of_ne_zero, coeff_order_eq_zero, order_of_ne, HahnModule.coeff_single_zero_smul, single_add, LaurentSeries.hasseDeriv_single_add, order_zero, coeff_single, support_single_of_ne, coeff_zero', single_zero_one, leadingCoeff_nonneg_iff, iterateEquiv_apply, leadingCoeff_eq_iff, PowerSeries.coe_X, SummableFamily.coe_zero, HahnModule.zero_smul', single_div_single, mk_eq_zero, inv_def, support_single_subset, RatFunc.single_one_eq_pow, SummableFamily.powers_toFun, coeff_mul_single, leadingCoeff_eq_zero, coeff_truncLT_of_lt, RatFunc.single_zpow, HVertexOperator.compHahnSeries_coeff, coeff_zero, HahnModule.of_symm_zero, HahnModule.of_zero, coeff_toOrderTopSubOnePos_pow, HahnEmbedding.Partial.eval_zero, single_eq_zero, min_le_min_add, coeff_mul_single_add, coeff_mul_single_zero, leadingCoeff_neg_iff, truncLT_smul, embDomain_zero, inv_single, C_apply, support_truncLT_subset, leadingCoeff_of_single, orderTop_zero, RatFunc.single_inv, zero_ofSuppBddBelow, single_zero_ratCast, HahnEmbedding.Partial.apply_of_mem_stratum, LaurentSeries.powerSeriesPart_zero, leadingCoeff_zero, leadingCoeff_nonpos_iff, single_zero_ofNat, SummableFamily.powerSeriesFamily_smul, iterateEquiv_symm_apply, leadingCoeff_of_ne_zero, SummableFamily.hsum_zero, LaurentSeries.hasseDeriv_single, SummableFamily.coe_ofFinsupp, order_single, coeff_single_mul, support_zero, orderTop_single, HahnModule.single_zero_smul_eq_smul, LaurentSeries.powerSeriesPart_eq_zero
|
iterateEquiv 📖 | CompOp | 2 mathmath: iterateEquiv_apply, iterateEquiv_symm_apply
|
leadingCoeff 📖 | CompOp | 33 mathmath: leadingCoeff_mul, coeff_untop_eq_leadingCoeff, leadingCoeff_sub, leadingCoeff_of_ne, HahnModule.coeff_smul_order_add_order, archimedeanClassMk_eq_archimedeanClassMk_iff, leadingCoeff_pos_iff, leadingCoeff_mul_of_ne_zero, coeff_mul_order_add_order, finiteArchimedeanClassOrderIsoLex_apply_snd, leadingCoeff_eq, isUnit_iff, archimedeanClassMk_le_archimedeanClassMk_iff_of_orderTop_ofLex, leadingCoeff_nonneg_iff, leadingCoeff_eq_iff, archimedeanClassMk_le_archimedeanClassMk_iff, inv_def, addOppositeEquiv_symm_leadingCoeff, addOppositeEquiv_leadingCoeff, leadingCoeff_one, leadingCoeff_neg, orderTop_self_sub_one_pos_iff, leadingCoeff_mul_of_nonzero, leadingCoeff_eq_zero, leadingCoeff_add_eq_right, leadingCoeff_neg_iff, leadingCoeff_add_eq_left, leadingCoeff_of_single, SummableFamily.hsum_leadingCoeff_of_le, leadingCoeff_zero, leadingCoeff_nonpos_iff, leadingCoeff_of_ne_zero, leadingCoeff_abs
|
map 📖 | CompOp | 12 mathmath: map_single, map_neg, cardSupp_map_le, map_C, map_mul, map_one, map_zero, map_sub, support_map_subset, map_add, map_smul, map_coeff
|
ofFinsupp 📖 | CompOp | 1 mathmath: coeff_ofFinsupp
|
ofIterate 📖 | CompOp | 2 mathmath: iterateEquiv_apply, HVertexOperator.comp_apply
|
ofSuppBddBelow 📖 | CompOp | 6 mathmath: ofSuppBddBelow_zero, ofSuppBddBelow_eq_zero, order_ofForallLtEqZero, coeff_ofSuppBddBelow, ofSuppBddBelow_coeff, zero_ofSuppBddBelow
|
orderTop 📖 | CompOp | 57 mathmath: untop_orderTop_of_ne_zero, orderTop_single_le, HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk, orderTop_sub_pos, orderTop_one, orderTop_of_subsingleton, orderTop_of_Subsingleton, orderTop_mul_of_nonzero, HahnEmbedding.Partial.orderTop_eq_iff, coeff_untop_eq_leadingCoeff, zero_lt_orderTop_of_order, orderTop_eq_top_iff, lt_orderTop_single, orderTop_of_ne, orderTop_le_of_coeff_ne_zero, leadingCoeff_of_ne, archimedeanClassMk_eq_archimedeanClassMk_iff, orderTop_lt_top, orderTop_eq_of_le, orderTop_mul_of_ne_zero, unit_aux, orderTop_eq_top, addOppositeEquiv_orderTop, orderTop_of_ne_zero, orderTop_mul, orderTop_nsmul_le_orderTop_pow, order_eq_orderTop_of_ne_zero, archimedeanClassOrderIsoWithTop_apply, orderTop_add_le_mul, HahnEmbedding.Partial.orderTop_eq_finiteArchimedeanClassMk, addOppositeEquiv_symm_orderTop, hahnEmbedding_isOrderedModule_rat, HahnModule.orderTop_vAdd_le_orderTop_smul, orderTop_le_orderTop_smul, orderTop_lt_iff_exists, archimedeanClassMk_le_archimedeanClassMk_iff, order_eq_orderTop_of_ne, orderTop_neg, SummableFamily.powers_toFun, orderTop_self_sub_one_pos_iff, min_orderTop_le_orderTop_sub, finiteArchimedeanClassOrderIsoLex_apply_fst, orderTop_abs, zero_lt_orderTop_iff, finiteArchimedeanClassOrderIso_apply, zero_le_orderTop_iff, orderTop_smul_not_lt, addVal_apply, orderTop_zero, mem_orderTopSubOnePos_iff, orderTop_embDomain, min_orderTop_le_orderTop_add, leadingCoeff_of_ne_zero, le_orderTop_iff_forall, hahnEmbedding_isOrderedAddMonoid, orderTop_single, hahnEmbedding_isOrderedModule
|
single 📖 | CompOp | 63 mathmath: orderTop_single_le, map_single, cardSupp_single_of_ne, HahnModule.coeff_single_smul_vadd, coeff_single_mul_add, orderTop_sub_pos, single_zero_natCast, single_zero_ofScientific, cardSupp_single_le, ofPowerSeries_X_pow, LaurentSeries.valuation_single_zpow, single_pow, coeff_single_same, single_zero_nnratCast, LaurentSeries.ofPowerSeries_powerSeriesPart, LaurentSeries.single_order_mul_powerSeriesPart, single_zero_intCast, RatFunc.coe_X, single_mul_single, single_zero_mul_eq_smul, single_sub, single_eq_zero_iff, order_single_mul_of_isRegular, coeff_single_zero_mul, embDomain_single, lt_orderTop_single, unit_aux, ofPowerSeries_X, coeff_single_of_ne, cardSupp_mul_single_le, cardSupp_single_mul_le, single_neg, single_injective, HahnModule.coeff_single_zero_smul, single_add, LaurentSeries.hasseDeriv_single_add, coeff_single, support_single_of_ne, single_zero_one, PowerSeries.coe_X, single_div_single, inv_def, support_single_subset, RatFunc.single_one_eq_pow, coeff_mul_single, RatFunc.single_zpow, coeff_toOrderTopSubOnePos_pow, single_eq_zero, coeff_mul_single_add, coeff_mul_single_zero, inv_single, C_apply, leadingCoeff_of_single, RatFunc.single_inv, single_zero_ratCast, HahnEmbedding.Partial.apply_of_mem_stratum, single_zero_ofNat, SummableFamily.powerSeriesFamily_smul, LaurentSeries.hasseDeriv_single, order_single, coeff_single_mul, orderTop_single, HahnModule.single_zero_smul_eq_smul
|
support 📖 | CompOp | 43 mathmath: SummableFamily.isPWO_iUnion_support', HahnModule.support_smul_subset_vadd_support', untop_orderTop_of_ne_zero, support_neg_subset, support_sub_subset, isPWO_support, addOppositeEquiv_symm_support, SummableFamily.support_hsum_subset, coeff_mul, SummableFamily.coeff_hsum_mul, support_abs, support_mk, addOppositeEquiv_support, SummableFamily.isPWO_iUnion_support, support_truncLT, SummableFamily.support_pow_subset_closure, orderTop_of_ne, embDomainAlgHom_apply_coeff, support_smul_subset, support_neg, support_eq_empty_iff, support_nonempty_iff, SummableFamily.coeff_smul, SummableFamily.isPWO_iUnion_support_powers, orderTop_of_ne_zero, HahnModule.coeff_smul, order_of_ne, support_single_of_ne, ofPowerSeriesAlg_apply_coeff, support_mul_subset_add_support, SummableFamily.sum_vAddAntidiagonal_eq, support_single_subset, support_map_subset, support_mul_subset, HahnModule.support_smul_subset_vadd_support, min_le_min_add, support_embDomain_subset, support_add_subset, support_truncLT_subset, isWF_support, mem_support, support_one, support_zero
|
toIterate 📖 | CompOp | 1 mathmath: iterateEquiv_symm_apply
|
truncLT 📖 | CompOp | 9 mathmath: cardSupp_truncLT_le, coe_truncLTLinearMap, truncLT_add, support_truncLT, coeff_truncLT, coeff_truncLT_of_le, coeff_truncLT_of_lt, truncLT_smul, support_truncLT_subset
|
unexpander 📖 | CompOp | — |
«term__⟦_⟧» 📖 | CompOp | — |
| Name | Category | Theorems |
|---|
HahnSeries 📖 | CompData | 417 mathmath: HahnModule.support_smul_subset_vadd_support', HahnSeries.SummableFamily.zero_apply, HahnEmbedding.IsPartial.baseEmbedding_le, HahnModule.smul_add, HahnSeries.instNoZeroDivisorsFinsuppNat, HahnSeries.untop_orderTop_of_ne_zero, HahnSeries.orderTop_single_le, HahnSeries.support_neg_subset, HahnSeries.map_single, HahnSeries.SummableFamily.embDomain_apply, HahnSeries.coeff_fun_eq_zero_iff, HahnSeries.mem_cardSuppLTSubfield, PowerSeries.heval_C, HahnSeries.cardSupp_single_of_ne, HahnSeries.C_injective, HahnSeries.order_neg, HahnSeries.SummableFamily.coe_neg, HahnSeries.SummableFamily.mul_toFun, HahnModule.coeff_single_smul_vadd, HahnSeries.leadingCoeff_mul, HahnSeries.coe_cardSuppLTAddSubmonoid, HahnSeries.support_sub_subset, HahnSeries.instIsStrictOrderedRingLexOfIsDomain, LaurentSeries.LaurentSeriesRingEquiv_def, HahnSeries.SummableFamily.ext_iff, HahnSeries.cardSupp_smul_le, HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk, HahnSeries.addOppositeEquiv_symm_support, HahnSeries.SummableFamily.powers_zero, HahnSeries.embDomain_smul, HahnSeries.coeff_single_mul_add, HahnSeries.orderTop_sub_pos, HahnSeries.single_zero_natCast, HahnSeries.single_zero_ofScientific, VertexOperator.of_coeff_apply_coeff, HahnSeries.cardSupp_single_le, HahnSeries.ofPowerSeries_X_pow, LaurentSeries.valuation_single_zpow, HahnSeries.single_pow, HahnSeries.instNontrivialOfNonempty, HahnSeries.embDomainLinearMap_apply, HVertexOperator.coeff_isPWOsupport, HahnSeries.SummableFamily.coe_add, HahnSeries.SummableFamily.add_apply, HahnModule.add_smul, HahnSeries.SummableFamily.support_hsum_subset, HahnSeries.single.addMonoidHom_apply_coeff, HahnSeries.instSMulCommClass, PowerSeries.coe_add, HahnSeries.SummableFamily.embDomain_notin_range, PowerSeries.coeff_heval, HahnSeries.coeff_single_same, HahnSeries.ofSuppBddBelow_zero, HahnSeries.single_zero_nnratCast, HahnSeries.SummableFamily.lsum_apply, HahnSeries.coeff_mul, HahnSeries.SummableFamily.coeff_hsum_mul, LaurentSeries.ofPowerSeries_powerSeriesPart, HahnSeries.SummableFamily.sub_apply, LaurentSeries.single_order_mul_powerSeriesPart, HahnEmbedding.Partial.archimedeanClassMk_eq_iff, HahnSeries.support_abs, HahnSeries.embDomainRingHom_apply, HahnSeries.le_orderTop_of_leadingCoeff_eq, HahnSeries.single.linearMap_apply, HahnEmbedding.Seed.baseEmbedding_strictMono, HahnSeries.map_neg, HahnSeries.single_zero_intCast, RatFunc.coe_X, HahnSeries.single_mul_single, PowerSeries.coeff_coe, HahnSeries.SummableFamily.hsum_smul_module, LaurentSeries.coe_algebraMap, HahnSeries.SummableFamily.powers_of_not_orderTop_pos, HahnSeries.single_zero_mul_eq_smul, RatFunc.coe_coe, HahnSeries.orderTop_one, HahnSeries.SummableFamily.smul_apply', HahnSeries.order_mul, HahnSeries.SummableFamily.Equiv_toFun, HahnSeries.coeff_mul_left', HahnSeries.toMvPowerSeries_symm_apply_coeff, PowerSeries.coe_smul, HahnSeries.SummableFamily.powerSeriesFamily_of_not_orderTop_pos, HahnEmbedding.Partial.toOrderAddMonoidHom_apply, HahnSeries.cardSupp_truncLT_le, HahnSeries.SummableFamily.smul_apply, HahnSeries.cardSupp_one_le, HahnSeries.instIsCancelMulZeroOfIsCancelAdd, HahnSeries.orderTop_mul_of_nonzero, HahnSeries.single_sub, HahnSeries.addOppositeEquiv_support, HahnEmbedding.Partial.orderTop_eq_iff, HahnSeries.SummableFamily.coe_powers, HahnSeries.SummableFamily.isPWO_iUnion_support, HahnSeries.SummableFamily.co_support_zero, HahnSeries.map_C, LaurentSeries.val_le_one_iff_eq_coe, HahnSeries.single_eq_zero_iff, HahnSeries.coeff_smul, HahnSeries.mem_cardSuppLTSubring, PowerSeries.coe_mul, HahnSeries.coeff_sub, HahnSeries.order_single_mul_of_isRegular, HahnSeries.coeff_single_zero_mul, HahnSeries.isUnit_of_isUnit_leadingCoeff_AddUnitOrder, HahnSeries.instNontrivialSubalgebra, PowerSeries.heval_apply, HahnSeries.addVal_le_of_coeff_ne_zero, PowerSeries.coe_sub, HahnSeries.embDomain_one, LaurentSeries.algebraMap_apply, HahnSeries.coe_truncLTLinearMap, HahnSeries.SummableFamily.coe_smul', HahnSeries.map_mul, HahnEmbedding.IsPartial.strictMono, HahnSeries.coeff_injective, HahnSeries.cardSuppLTSubfield_carrier, HahnSeries.coeff_smul', HahnSeries.coeff_sum, HahnSeries.SummableFamily.single_toFun, HahnSeries.SummableFamily.smul_hsum, HahnSeries.SummableFamily.embDomain_succ_smul_powers, HahnSeries.SummableFamily.smul_support_subset_prod, HahnSeries.SummableFamily.hsum_add, HahnSeries.leadingCoeff_sub, HahnSeries.embDomainOrderEmbedding_apply, HahnSeries.embDomain_injective, HahnSeries.orderTop_eq_top_iff, HahnSeries.of_symm_smul_of_eq_mul, HahnSeries.SummableFamily.smul_toFun, HahnEmbedding.IsPartial.truncLT_mem_range, HahnSeries.SummableFamily.smul_support_finite, HahnSeries.truncLT_add, HahnSeries.cardSupp_neg_le, HahnSeries.embDomainRingHom_C, HahnSeries.mem_cardSuppLTAddSubgroup, HahnSeries.order_abs, HahnSeries.support_truncLT, HahnSeries.embDomain_single, HahnSeries.SummableFamily.support_pow_subset_closure, HahnSeries.SummableFamily.coe_injective, HahnSeries.SummableFamily.const_toFun, HahnSeries.coeff_neg, HahnSeries.lt_orderTop_single, HahnSeries.orderTop_of_ne, HahnSeries.coeff_truncLT, HahnSeries.algebraMap_apply, HahnSeries.cardSupp_neg, HahnSeries.ofSuppBddBelow_eq_zero, HahnSeries.SummableFamily.coeff_support, HahnSeries.order_mul_of_nonzero, HahnSeries.map_one, HVertexOperator.compHahnSeries_smul, HahnSeries.leadingCoeff_of_ne, HahnModule.coeff_smul_order_add_order, HahnModule.of_symm_smul, HahnSeries.coe_cardSuppLTAddSubgroup, HahnModule.instIsScalarTowerHahnSeries_1, HahnSeries.SummableFamily.powerSeriesFamily_hsum_zero, HahnSeries.archimedeanClassMk_eq_archimedeanClassMk_iff, HahnSeries.SummableFamily.smul_eq, HahnSeries.leadingCoeff_pos_iff, HahnSeries.C_eq_algebraMap, HahnSeries.instNoZeroDivisors, HahnSeries.leadingCoeff_mul_of_ne_zero, HahnSeries.ofPowerSeries_apply_coeff, HahnSeries.embDomainAlgHom_apply_coeff, HahnSeries.coeff_mul_order_add_order, HahnEmbedding.Partial.eval_smul, HahnSeries.orderTop_mul_of_ne_zero, HahnSeries.unit_aux, HahnSeries.support_smul_subset, HahnSeries.orderTop_eq_top, HahnSeries.ofPowerSeries_X, LaurentSeries.coe_X_compare, HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_snd, HahnSeries.cardSupp_div_le, HahnSeries.coeff_single_of_ne, HahnModule.SMulCommClass, LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero, HahnSeries.SummableFamily.hsum_ofFinsupp, HahnSeries.support_neg, HahnSeries.cardSupp_mul_single_le, HahnSeries.C_zero, HahnSeries.addVal_apply_of_ne, HVertexOperator.compHahnSeries_add, PowerSeries.coe_zero, HahnSeries.coeff_truncLT_of_le, HahnSeries.toPowerSeriesAlg_apply, HahnSeries.isUnit_iff, HahnSeries.toPowerSeriesAlg_symm_apply_coeff, HahnSeries.cardSupp_single_mul_le, HahnSeries.support_eq_empty_iff, HahnSeries.min_order_le_order_add, LaurentSeries.exists_powerSeries_of_memIntegers, HahnSeries.coeff_ofFinsupp, HahnSeries.SummableFamily.coe_mk, HahnModule.ext_iff, HahnSeries.binomial_power, HahnSeries.map_zero, PowerSeries.coe_C, HahnModule.of_symm_add, HahnSeries.single_neg, PowerSeries.coe_neg, HahnSeries.SummableFamily.coeff_smul, HahnSeries.SummableFamily.coe_sub, HahnSeries.addOppositeEquiv_orderTop, HahnSeries.embDomainOrderAddMonoidHom_injective, HahnSeries.single_injective, HahnSeries.cardSupp_zero, HahnSeries.SummableFamily.isPWO_iUnion_support_powers, HahnSeries.orderTop_of_ne_zero, HahnModule.coeff_smul, HahnSeries.pow_add, HahnSeries.orderTop_mul, HahnSeries.coeff_toPowerSeries, HahnSeries.embDomain_add, HahnSeries.coeff_order_eq_zero, HahnSeries.order_of_ne, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, HahnModule.coeff_single_zero_smul, HahnSeries.single_add, LaurentSeries.hasseDeriv_single_add, HahnSeries.orderTop_nsmul_le_orderTop_pow, HahnSeries.order_zero, HahnSeries.archimedeanClassOrderIsoWithTop_apply, HahnSeries.coeff_one, HahnSeries.coeff_single, HahnSeries.coeff_toPowerSeries_symm, HahnSeries.order_smul_not_lt, HahnSeries.support_single_of_ne, LaurentSeries.powerSeriesRingEquiv_coe_apply, HahnSeries.orderTop_add_le_mul, HahnSeries.coeff_zero', HahnSeries.ofPowerSeriesAlg_apply_coeff, LaurentSeries.powerSeriesEquivSubring_apply, HahnSeries.single_zero_one, HahnSeries.SummableFamily.smulFamily_toFun, HahnSeries.leadingCoeff_nonneg_iff, PowerSeries.heval_X, HahnSeries.coeff_add, HahnEmbedding.Partial.orderTop_eq_finiteArchimedeanClassMk, HahnSeries.addOppositeEquiv_symm_orderTop, HahnSeries.SummableFamily.one_sub_self_mul_hsum_powers, HahnSeries.iterateEquiv_apply, hahnEmbedding_isOrderedModule_rat, HahnSeries.map_sub, HahnSeries.mem_cardSuppLTAddSubmonoid, HahnSeries.support_mul_subset_add_support, Polynomial.algebraMap_hahnSeries_apply, HahnModule.orderTop_vAdd_le_orderTop_smul, HahnSeries.coeff_sub', HahnSeries.coeff_toMvPowerSeries_symm, HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding, HahnSeries.SummableFamily.neg_apply, HahnSeries.orderTop_le_orderTop_smul, HahnEmbedding.Partial.mem_domain, HahnSeries.SummableFamily.coeff_hsum, HahnSeries.embDomain_mul, LaurentSeries.powerSeriesEquivSubring_coe_apply, HahnSeries.embDomainOrderAddMonoidHom_apply, HahnEmbedding.Seed.mem_domain_baseEmbedding, HahnSeries.leadingCoeff_eq_iff, PowerSeries.coe_X, HahnSeries.SummableFamily.coe_zero, HahnModule.zero_smul', HahnSeries.coeff_neg', HahnSeries.single_div_single, Polynomial.algebraMap_hahnSeries_injective, HahnSeries.mk_eq_zero, HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff, HahnSeries.instSubsingleton, HahnSeries.inv_def, HahnSeries.addOppositeEquiv_symm_leadingCoeff, HahnSeries.addOppositeEquiv_leadingCoeff, HahnSeries.SummableFamily.sum_vAddAntidiagonal_eq, HahnSeries.coeff_mul_right', HahnSeries.support_single_subset, HahnSeries.leadingCoeff_one, HahnSeries.lt_iff, HahnSeries.instIsOrderedAddMonoidLex, HahnSeries.C_mul_eq_smul, HahnSeries.SummableFamily.powerSeriesFamily_of_orderTop_pos, HahnModule.one_smul', HahnSeries.orderTop_neg, RatFunc.single_one_eq_pow, HahnSeries.SummableFamily.powers_toFun, HahnModule.of_smul, PowerSeries.heval_unit, HahnSeries.coeff_toMvPowerSeries, HahnSeries.leadingCoeff_neg, HahnSeries.coeff.linearMap_apply, HahnSeries.orderTop_self_sub_one_pos_iff, HahnSeries.coeff_mul_single, HahnSeries.cardSupp_add_le, HahnSeries.SummableFamily.hsum_smul, HahnSeries.min_orderTop_le_orderTop_sub, HahnSeries.C_one, HahnSeries.SummableFamily.hsum_mul, HahnModule.of_sub, HahnSeries.map_add, HahnModule.of_add, HahnSeries.support_mul_subset, HahnSeries.leadingCoeff_mul_of_nonzero, HahnSeries.leadingCoeff_eq_zero, HahnSeries.order_pow, HahnSeries.instIsScalarTower, HahnSeries.order_C, HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_fst, HahnSeries.coeff_truncLT_of_lt, HahnModule.support_smul_subset_vadd_support, RatFunc.single_zpow, HahnSeries.orderTop_abs, HVertexOperator.compHahnSeries_coeff, HahnSeries.map_smul, HahnSeries.order_one, HahnSeries.instIsOrderedRingLexOfNoZeroDivisors, HahnSeries.coeff_zero, HahnSeries.leadingCoeff_add_eq_right, HahnSeries.SummableFamily.hsum_smulFamily, HahnModule.of_symm_zero, HahnSeries.ofPowerSeries_apply, HahnModule.of_zero, HahnModule.instIsScalarTowerHahnSeries, HahnSeries.toMvPowerSeries_apply, PowerSeries.coe_one, HahnSeries.SummableFamily.coeff_apply, HahnSeries.coeff_toOrderTopSubOnePos_pow, HahnSeries.SummableFamily.hsum_unique, HahnSeries.addOppositeEquiv_symm_apply_coeff, HVertexOperator.coeff_apply_apply, HVertexOperator.of_coeff_apply, HahnEmbedding.Partial.eval_zero, HahnSeries.single_eq_zero, HahnModule.coeff_smul_left, HahnSeries.finiteArchimedeanClassOrderIso_apply, PowerSeries.coeff_heval_zero, HahnSeries.instIsDomainOfIsCancelAdd, HahnSeries.ofPowerSeries_injective, HahnSeries.min_le_min_add, HahnSeries.coeff_mul_single_add, HahnSeries.orderTop_add_eq_left, HahnSeries.coeff_mul_single_zero, HahnSeries.SummableFamily.embDomain_image, HahnSeries.addOppositeEquiv_apply, HahnSeries.leadingCoeff_neg_iff, HahnSeries.truncLT_smul, HahnSeries.order_mul_of_ne_zero, HahnSeries.orderTop_add_eq_right, HahnSeries.embDomain_zero, HahnSeries.support_add_subset, HahnSeries.SummableFamily.powers_of_orderTop_pos, HahnSeries.inv_single, HahnSeries.C_apply, HahnModule.instIsTorsionFree, HahnSeries.leadingCoeff_add_eq_left, HahnSeries.support_truncLT_subset, HahnSeries.ofPowerSeries_C, PowerSeries.coe_pow, HahnSeries.orderTop_smul_not_lt, HahnSeries.cardSupp_sub_le, HahnSeries.addVal_apply, HahnEmbedding.Partial.exists_domain_eq_top, LaurentSeries.mem_integers_of_powerSeries, HahnSeries.toPowerSeries_apply, HahnSeries.coeff_nsmul, HahnSeries.leadingCoeff_of_single, HahnSeries.orderTop_zero, RatFunc.single_inv, PowerSeries.heval_mul, HahnSeries.SummableFamily.hsum_sub, HahnSeries.algebraMap_apply', HahnSeries.zero_ofSuppBddBelow, HahnSeries.SummableFamily.coeff_hsum_eq_sum, LaurentSeries.X_order_mul_powerSeriesPart, HahnSeries.mem_orderTopSubOnePos_iff, HahnSeries.single_zero_ratCast, HahnSeries.SummableFamily.coeff_def, HahnSeries.coeff.addMonoidHom_apply, HahnSeries.toPowerSeries_symm_apply_coeff, LaurentSeries.coeff_coe_powerSeries, HahnEmbedding.Partial.exists_isMax, HahnSeries.cardSupp_inv_le, HahnSeries.coeff_add', HahnSeries.min_orderTop_le_orderTop_add, HVertexOperator.comp_apply, HahnSeries.leadingCoeff_zero, HahnSeries.leadingCoeff_nonpos_iff, HahnSeries.single_zero_ofNat, HahnSeries.SummableFamily.powerSeriesFamily_smul, HahnSeries.orderTop_sub, HahnEmbedding.Seed.domain_baseEmbedding, HahnSeries.cardSupp_hsum_le, HahnSeries.iterateEquiv_symm_apply, HahnSeries.leadingCoeff_of_ne_zero, HahnSeries.support_one, HahnSeries.SummableFamily.finite_co_support, LaurentSeries.valuation_X_pow, HahnSeries.le_order_smul, HahnSeries.SummableFamily.hsum_zero, HahnSeries.cardSupp_one, LaurentSeries.hasseDeriv_single, HahnSeries.SummableFamily.coe_ofFinsupp, HahnSeries.order_single, HahnSeries.coeff_single_mul, hahnEmbedding_isOrderedAddMonoid, HahnSeries.coeff_ofFinsuppLinearMap, HahnSeries.cardSupp_pow_le, HahnSeries.support_zero, HahnSeries.orderTop_single, HahnSeries.leadingCoeff_abs, HahnModule.single_zero_smul_eq_smul, HahnSeries.cardSupp_mul_le, HahnModule.of_symm_sub, hahnEmbedding_isOrderedModule, HahnEmbedding.Partial.toOrderAddMonoidHom_injective
|