Summable

📁 Source: Mathlib/RingTheory/HahnSeries/Summable.lean

Statistics

Metric	Count
Definitions SummableFamily, coeff, const, embDomain, hsum, instAdd, instAddCommGroup, instAddCommMonoid, instFunLike, instInhabited, instModule, instNeg, instSMul, instSMul_1, instSub, instZero, lsum, mul, ofFinsupp, powers, single, smul, smulFamily, toFun, instDivInvMonoid, instField, toOrderTopSubOnePos, Summable	28
Theorems Equiv_toFun, add_apply, co_support_zero, coe_add, coe_injective, coe_mk, coe_neg, coe_ofFinsupp, coe_powers, coe_smul', coe_sub, coe_zero, coeff_apply, coeff_def, coeff_hsum, coeff_hsum_eq_sum, coeff_hsum_eq_sum_of_subset, coeff_hsum_mul, coeff_smul, coeff_support, const_toFun, embDomain_apply, embDomain_image, embDomain_notin_range, embDomain_succ_smul_powers, ext, ext_iff, finite_co_support, finite_co_support', finite_co_support_prod_mul, finite_co_support_prod_smul, hsum_add, hsum_embDomain, hsum_equiv, hsum_leadingCoeff_of_le, hsum_mul, hsum_ofFinsupp, hsum_orderTop_of_le, hsum_single, hsum_smul, hsum_smulFamily, hsum_smul_module, hsum_sub, hsum_unique, hsum_zero, isPWO_iUnion_support, isPWO_iUnion_support', isPWO_iUnion_support_powers, isPWO_iUnion_support_prod_mul, isPWO_iUnion_support_prod_smul, le_hsum_support_mem, lsum_apply, mul_eq_smul, mul_toFun, neg_apply, one_sub_self_mul_hsum_powers, pow_finite_co_support, powers_of_not_orderTop_pos, powers_of_orderTop_pos, powers_toFun, powers_zero, single_toFun, smulFamily_toFun, smul_apply, smul_apply', smul_eq, smul_hsum, smul_support_finite, smul_support_subset_prod, smul_toFun, sub_apply, sum_vAddAntidiagonal_eq, support_hsum_subset, support_pow_subset_closure, zero_apply, inv_def, inv_single, isUnit_iff, isUnit_of_isUnit_leadingCoeff_AddUnitOrder, isUnit_of_orderTop_pos, one_minus_single_neg_mul, single_div_single, single_zero_ofScientific, unit_aux, val_inv_toOrderTopSubOnePos_coe, val_toOrderTopSubOnePos_coe	86
Total	114

HahnSeries

Definitions

Name	Category	Theorems
SummableFamily 📖	CompData	57 math math: SummableFamily.powerSeriesFamily_add, SummableFamily.zero_apply, SummableFamily.embDomain_apply, SummableFamily.coe_neg, SummableFamily.mul_toFun, SummableFamily.ext_iff, SummableFamily.binomialFamily_orderTop_pos, SummableFamily.coe_add, SummableFamily.add_apply, SummableFamily.support_hsum_subset, SummableFamily.embDomain_notin_range, SummableFamily.binomialFamily_apply_of_orderTop_nonpos, SummableFamily.lsum_apply, SummableFamily.coeff_hsum_mul, SummableFamily.sub_apply, SummableFamily.hsum_smul_module, SummableFamily.smul_apply', SummableFamily.Equiv_toFun, SummableFamily.smul_apply, SummableFamily.coe_powers, SummableFamily.isPWO_iUnion_support, SummableFamily.coe_smul', SummableFamily.single_toFun, SummableFamily.embDomain_succ_smul_powers, SummableFamily.smul_support_subset_prod, SummableFamily.hsum_add, SummableFamily.smul_toFun, SummableFamily.smul_support_finite, SummableFamily.coe_injective, SummableFamily.const_toFun, SummableFamily.coeff_support, SummableFamily.smul_eq, SummableFamily.coe_mk, SummableFamily.coeff_smul, SummableFamily.coe_sub, SummableFamily.smulFamily_toFun, SummableFamily.binomialFamily_apply, SummableFamily.neg_apply, SummableFamily.coeff_hsum, SummableFamily.coe_zero, SummableFamily.sum_vAddAntidiagonal_eq, SummableFamily.powerSeriesFamily_of_orderTop_pos, SummableFamily.powers_toFun, SummableFamily.hsum_smul, SummableFamily.hsum_smulFamily, SummableFamily.coeff_apply, SummableFamily.hsum_unique, SummableFamily.embDomain_image, SummableFamily.powers_of_orderTop_pos, SummableFamily.hsum_sub, SummableFamily.coeff_hsum_eq_sum, SummableFamily.coeff_def, SummableFamily.powerSeriesFamily_smul, cardSupp_hsum_le, SummableFamily.finite_co_support, SummableFamily.hsum_zero, SummableFamily.coe_ofFinsupp
instDivInvMonoid 📖	CompOp	6 math math: cardSupp_div_le, RatFunc.algebraMap_apply_div, single_div_single, inv_def, RatFunc.single_zpow, inv_single
instField 📖	CompOp	16 math math: mem_cardSuppLTSubfield, RatFunc.coe_X, RatFunc.coe_coe, LaurentSeries.inducing_coe, LaurentSeries.continuous_coe, cardSuppLTSubfield_carrier, LaurentSeries.exists_ratFunc_val_lt, RatFunc.valuation_eq_LaurentSeries_valuation, RatFunc.algebraMap_apply_div, LaurentSeries.LaurentSeries_coe, LaurentSeries.valuation_coe_ratFunc, LaurentSeries.coe_range_dense, LaurentSeries.comparePkg_eq_extension, LaurentSeries.valuation_def, RatFunc.single_inv, cardSupp_inv_le
toOrderTopSubOnePos 📖	CompOp	4 math math: binomial_power, coeff_toOrderTopSubOnePos_pow, val_toOrderTopSubOnePos_coe, val_inv_toOrderTopSubOnePos_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inv_def 📖	mathematical	—	HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing DivInvMonoid.toInv instDivInvMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instMul AddCommGroup.toAddCommMonoid DFunLike.coe ZeroHom instZero ZeroHom.funLike single NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid order NegZeroClass.toZero InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield leadingCoeff SummableFamily.hsum SummableFamily.powers instSub AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	—
inv_single 📖	mathematical	—	HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing DivInvMonoid.toInv instDivInvMonoid DFunLike.coe ZeroHom instZero ZeroHom.funLike single NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield	—	eq_or_ne IsOrderedAddMonoid.toIsOrderedCancelAddMonoid map_zero ZeroHom.zeroHomClass order_zero neg_zero leadingCoeff_zero inv_zero SummableFamily.powers.congr_simp MulZeroClass.mul_zero sub_zero MulZeroClass.zero_mul order_single leadingCoeff_of_single single_mul_single neg_add_cancel inv_mul_cancel₀ sub_self SummableFamily.powers_zero SummableFamily.hsum_single mul_one
isUnit_iff 📖	mathematical	—	IsUnit HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring AddCommGroup.toAddCommMonoid IsOrderedAddMonoid.toIsOrderedCancelAddMonoid CommSemiring.toSemiring CommRing.toCommSemiring leadingCoeff	—	IsOrderedAddMonoid.toIsOrderedCancelAddMonoid IsUnit.of_mul_eq_one instIsDedekindFiniteMonoid coeff_mul_order_add_order coeff_one order_mul IsDomain.to_noZeroDivisors left_ne_zero_of_mul_eq_one instNontrivialOfNonempty Zero.instNonempty IsDomain.toNontrivial right_ne_zero_of_mul_eq_one order_one SummableFamily.one_sub_self_mul_hsum_powers unit_aux neg_add_cancel isUnit_of_mul_isUnit_right sub_sub_cancel
isUnit_of_isUnit_leadingCoeff_AddUnitOrder 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring leadingCoeff SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsAddUnit AddCommMonoid.toAddMonoid order AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	HahnSeries instSemiring	—	SummableFamily.one_sub_self_mul_hsum_powers unit_aux AddUnits.neg_add isUnit_of_mul_isUnit_right instIsDedekindFiniteMonoid IsUnit.of_mul_eq_one sub_sub_cancel
isUnit_of_orderTop_pos 📖	mathematical	WithTop Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithTop.zero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid orderTop MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing HahnSeries instSub AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring CommSemiring.toSemiring CommRing.toCommSemiring	—	subsingleton_or_nontrivial isUnit_of_subsingleton instSubsingleton isUnit_of_isUnit_leadingCoeff_AddUnitOrder orderTop_self_sub_one_pos_iff isUnit_one WithTop.coe_eq_zero order_eq_orderTop_of_ne_zero WithTop.top_ne_zero orderTop_eq_top isAddUnit_zero
one_minus_single_neg_mul 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing leadingCoeff SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing HahnSeries instAdd AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DFunLike.coe ZeroHom instZero ZeroHom.funLike single order AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	instSub AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup instOne instMul instNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	mul_add Distrib.leftDistribClass single_mul_single sub_add_eq_sub_sub_swap sub_eq_neg_self sub_eq_zero_of_eq single_zero_one
single_div_single 📖	mathematical	—	HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing DivInvMonoid.toDiv instDivInvMonoid DFunLike.coe ZeroHom instZero ZeroHom.funLike single SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DivisionRing.toDivInvMonoid Field.toDivisionRing	—	div_eq_mul_inv sub_eq_add_neg inv_single single_mul_single
single_zero_ofScientific 📖	mathematical	—	DFunLike.coe ZeroHom HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing instZero ZeroHom.funLike single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NNRatCast.toOfScientific DivisionRing.toNNRatCast Field.toDivisionRing instNNRatCast	—	Rat.cast_ofScientific single_zero_ratCast
unit_aux 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing leadingCoeff SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup order AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	WithTop Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder WithTop.zero orderTop HahnSeries instSub AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup instOne instMul DFunLike.coe ZeroHom instZero ZeroHom.funLike single	—	eq_of_sub_eq_zero single_mul_single single_zero_one sub_self orderTop_zero IsUnit.isRegular IsUnit.of_mul_eq_one instIsDedekindFiniteMonoid order_single_mul_of_isRegular pos_of_lt_add_right contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid add_assoc add_comm zero_add order_lt_order_of_eq_add_single sub_add_cancel one_minus_single_neg_mul orderTop_neg zero_lt_orderTop_of_order
val_inv_toOrderTopSubOnePos_coe 📖	mathematical	WithTop Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithTop.zero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid orderTop MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing HahnSeries instSub AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring CommSemiring.toSemiring CommRing.toCommSemiring Units Units.instInv Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike orderTopSubOnePos toOrderTopSubOnePos Units.inv IsUnit.unit isUnit_of_orderTop_pos	—	—
val_toOrderTopSubOnePos_coe 📖	mathematical	WithTop Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithTop.zero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid orderTop MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing HahnSeries instSub AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring CommSemiring.toSemiring CommRing.toCommSemiring Units Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike orderTopSubOnePos toOrderTopSubOnePos	—	—

HahnSeries.SummableFamily

Definitions

Name	Category	Theorems
coeff 📖	CompOp	6 math math: PowerSeries.coeff_heval, coeff_support, coeff_apply, support_powerSeriesFamily_subset, coeff_hsum_eq_sum, coeff_def
const 📖	CompOp	2 math math: const_toFun, smul_eq
embDomain 📖	CompOp	5 math math: embDomain_apply, embDomain_notin_range, embDomain_succ_smul_powers, hsum_embDomain, embDomain_image
hsum 📖	CompOp	31 math math: hsum_orderTop_of_le, coeff_hsum_eq_sum_of_subset, support_hsum_subset, lsum_apply, coeff_hsum_mul, hsum_smul_module, hsum_powerSeriesFamily_mul, PowerSeries.heval_apply, smul_hsum, hsum_add, powerSeriesFamily_hsum_zero, hsum_embDomain, hsum_ofFinsupp, orderTop_hsum_binomialFamily_pos, HahnSeries.binomial_power, coeff_smul, hsum_single, one_sub_self_mul_hsum_powers, coeff_hsum, HahnSeries.inv_def, hsum_smul, hsum_mul, hsum_smulFamily, hsum_unique, hsum_equiv, HahnSeries.cardSupp_hsum_powers_le, hsum_sub, coeff_hsum_eq_sum, hsum_leadingCoeff_of_le, HahnSeries.cardSupp_hsum_le, hsum_zero
instAdd 📖	CompOp	4 math math: powerSeriesFamily_add, coe_add, add_apply, hsum_add
instAddCommGroup 📖	CompOp	—
instAddCommMonoid 📖	CompOp	1 math math: lsum_apply
instFunLike 📖	CompOp	47 math math: zero_apply, embDomain_apply, coe_neg, mul_toFun, ext_iff, binomialFamily_orderTop_pos, coe_add, add_apply, support_hsum_subset, embDomain_notin_range, binomialFamily_apply_of_orderTop_nonpos, coeff_hsum_mul, sub_apply, smul_apply', Equiv_toFun, smul_apply, coe_powers, isPWO_iUnion_support, coe_smul', single_toFun, smul_support_subset_prod, smul_toFun, smul_support_finite, coe_injective, const_toFun, coeff_support, coe_mk, coeff_smul, coe_sub, smulFamily_toFun, binomialFamily_apply, neg_apply, coeff_hsum, coe_zero, sum_vAddAntidiagonal_eq, powerSeriesFamily_of_orderTop_pos, powers_toFun, hsum_smulFamily, coeff_apply, hsum_unique, embDomain_image, powers_of_orderTop_pos, coeff_hsum_eq_sum, coeff_def, HahnSeries.cardSupp_hsum_le, finite_co_support, coe_ofFinsupp
instInhabited 📖	CompOp	—
instModule 📖	CompOp	1 math math: lsum_apply
instNeg 📖	CompOp	2 math math: coe_neg, neg_apply
instSMul 📖	CompOp	2 math math: smul_apply', coe_smul'
instSMul_1 📖	CompOp	6 math math: hsum_smul_module, smul_apply, embDomain_succ_smul_powers, smul_eq, hsum_smul, powerSeriesFamily_smul
instSub 📖	CompOp	4 math math: sub_apply, embDomain_succ_smul_powers, coe_sub, hsum_sub
instZero 📖	CompOp	3 math math: zero_apply, coe_zero, hsum_zero
lsum 📖	CompOp	1 math math: lsum_apply
mul 📖	CompOp	6 math math: mul_toFun, coeff_hsum_mul, hsum_powerSeriesFamily_mul, hsum_mul, support_powerSeriesFamily_subset, mul_eq_smul
ofFinsupp 📖	CompOp	3 math math: embDomain_succ_smul_powers, hsum_ofFinsupp, coe_ofFinsupp
powers 📖	CompOp	9 math math: powers_zero, powers_of_not_orderTop_pos, coe_powers, embDomain_succ_smul_powers, one_sub_self_mul_hsum_powers, HahnSeries.inv_def, powers_toFun, powers_of_orderTop_pos, HahnSeries.cardSupp_hsum_powers_le
single 📖	CompOp	4 math math: powers_zero, powers_of_not_orderTop_pos, single_toFun, hsum_single
smul 📖	CompOp	5 math math: smul_hsum, smul_toFun, smul_eq, coeff_smul, mul_eq_smul
smulFamily 📖	CompOp	2 math math: smulFamily_toFun, hsum_smulFamily
toFun 📖	CompOp	4 math math: isPWO_iUnion_support', smul_support_subset_prod, sum_vAddAntidiagonal_eq, finite_co_support'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Equiv_toFun 📖	mathematical	—	DFunLike.coe HahnSeries.SummableFamily HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike Equiv Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	—
add_apply 📖	mathematical	—	DFunLike.coe HahnSeries.SummableFamily HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike instAdd HahnSeries.instAdd	—	—
co_support_zero 📖	mathematical	—	Set Set.instHasSubset setOf HahnSeries.coeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring HahnSeries Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero HahnSeries.instSemiring HahnSeries.instZero Set.instSingletonSet	—	zero_pow
coe_add 📖	mathematical	—	DFunLike.coe HahnSeries.SummableFamily HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike instAdd Pi.instAdd HahnSeries.instAdd	—	—
coe_injective 📖	mathematical	—	HahnSeries.SummableFamily DFunLike.coe HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike	—	DFunLike.coe_injective
coe_mk 📖	mathematical	Set.IsPWO PartialOrder.toPreorder Set.iUnion HahnSeries.support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Set.Finite setOf HahnSeries.coeff	DFunLike.coe HahnSeries.SummableFamily HahnSeries instFunLike	—	—
coe_neg 📖	mathematical	—	DFunLike.coe HahnSeries.SummableFamily AddCommGroup.toAddCommMonoid HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike instNeg Pi.instNeg HahnSeries.instNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
coe_ofFinsupp 📖	mathematical	—	DFunLike.coe HahnSeries.SummableFamily HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike ofFinsupp Finsupp HahnSeries.instZero Finsupp.instFunLike	—	—
coe_powers 📖	mathematical	WithTop Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithTop.zero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid HahnSeries.orderTop MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	DFunLike.coe HahnSeries.SummableFamily NonUnitalNonAssocSemiring.toAddCommMonoid HahnSeries instFunLike powers Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero HahnSeries.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring	—	—
coe_smul' 📖	mathematical	—	DFunLike.coe HahnSeries.SummableFamily HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike instSMul Function.hasSMul HahnSeries.instSMul	—	—
coe_sub 📖	mathematical	—	DFunLike.coe HahnSeries.SummableFamily AddCommGroup.toAddCommMonoid HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike instSub Pi.instSub HahnSeries.instSub AddCommGroup.toAddGroup	—	—
coe_zero 📖	mathematical	—	DFunLike.coe HahnSeries.SummableFamily HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike instZero Pi.instZero HahnSeries.instZero	—	—
coeff_apply 📖	mathematical	—	DFunLike.coe Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instFunLike coeff HahnSeries.coeff HahnSeries.SummableFamily HahnSeries instFunLike	—	—
coeff_def 📖	mathematical	—	DFunLike.coe Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instFunLike coeff HahnSeries.coeff HahnSeries.SummableFamily HahnSeries instFunLike	—	—
coeff_hsum 📖	mathematical	—	HahnSeries.coeff AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid hsum finsum DFunLike.coe HahnSeries.SummableFamily HahnSeries instFunLike	—	—
coeff_hsum_eq_sum 📖	mathematical	—	HahnSeries.coeff AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid hsum Finset.sum Finsupp.support coeff DFunLike.coe HahnSeries.SummableFamily HahnSeries instFunLike	—	finite_co_support finsum_eq_sum
coeff_hsum_eq_sum_of_subset 📖	mathematical	Set Set.instHasSubset setOf HahnSeries.coeff AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe HahnSeries.SummableFamily HahnSeries instFunLike SetLike.coe Finset Finset.instSetLike	hsum Finset.sum	—	finite_co_support finsum_eq_sum Finset.sum_subset Set.Finite.toFinset_subset
coeff_hsum_mul 📖	mathematical	—	HahnSeries.coeff AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring hsum mul Finset.sum Finset.addAntidiagonal Set.iUnion HahnSeries.support DFunLike.coe HahnSeries.SummableFamily HahnSeries instFunLike isPWO_iUnion_support Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	isPWO_iUnion_support Finset.sum_congr coeff_smul instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid
coeff_smul 📖	mathematical	—	HahnSeries.coeff AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid hsum smul NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulActionWithZero.toSMulWithZero Semiring.toMonoidWithZero Module.toMulActionWithZero Finset.sum Finset.VAddAntidiagonal Set.iUnion HahnSeries.support DFunLike.coe HahnSeries.SummableFamily HahnSeries instFunLike isPWO_iUnion_support SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction	—	isPWO_iUnion_support coeff_hsum HahnSeries.isPWO_support Equiv.symm_apply_apply Finset.sum_congr Finset.VAddAntidiagonal.congr_simp coeff_hsum_eq_sum isPWO_iUnion_support' HahnSeries.isPWO_support' sum_vAddAntidiagonal_eq Finset.smul_sum Finset.sum_smul sum_finsum_comm smul_support_finite finsum_eq_sum Finset.sum_product_right' Finset.sum_subset Set.Finite.prod finite_co_support' smul_support_subset_prod finite_co_support Set.Finite.coe_toFinset
coeff_support 📖	mathematical	—	Finsupp.support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid coeff Set.Finite.toFinset Function.support HahnSeries.coeff DFunLike.coe HahnSeries.SummableFamily HahnSeries instFunLike finite_co_support	—	—
const_toFun 📖	mathematical	—	DFunLike.coe HahnSeries.SummableFamily HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike const	—	—
embDomain_apply 📖	mathematical	—	DFunLike.coe HahnSeries.SummableFamily HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike embDomain Set Set.instMembership Set.range Function.Embedding Function.instFunLikeEmbedding HahnSeries.instZero	—	—
embDomain_image 📖	mathematical	—	DFunLike.coe HahnSeries.SummableFamily HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike embDomain Function.Embedding Function.instFunLikeEmbedding	—	embDomain_apply Set.mem_range_self Function.Embedding.injective
embDomain_notin_range 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding	HahnSeries.SummableFamily HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike embDomain HahnSeries.instZero	—	embDomain_apply
embDomain_succ_smul_powers 📖	mathematical	WithTop Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithTop.zero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid HahnSeries.orderTop MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	embDomain NonUnitalNonAssocSemiring.toAddCommMonoid HahnSeries HahnSeries.SummableFamily instSMul_1 MulZeroClass.toSMulWithZero AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction AddMonoid.toAddAction instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid powers Nat.succ_injective instSub Ring.toAddCommGroup CommRing.toRing ofFinsupp Finsupp.single HahnSeries.instZero HahnSeries.instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	ext instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid Nat.succ_injective embDomain_notin_range Nat.range_succ coe_powers pow_zero Finsupp.single_eq_same sub_self IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd Nat.instZeroLEOneClass Classical.choose_eq powers_of_orderTop_pos pow_succ' Finsupp.single_eq_of_ne sub_zero
ext 📖	—	DFunLike.coe HahnSeries.SummableFamily HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe HahnSeries.SummableFamily HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike	—	ext
finite_co_support 📖	mathematical	—	Set.Finite Function.support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid HahnSeries.coeff DFunLike.coe HahnSeries.SummableFamily HahnSeries instFunLike	—	finite_co_support'
finite_co_support' 📖	mathematical	—	Set.Finite setOf HahnSeries.coeff AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid toFun	—	—
finite_co_support_prod_mul 📖	mathematical	—	Finite Set.Elem setOf HahnSeries.coeff AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	finite_co_support_prod_smul instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid
finite_co_support_prod_smul 📖	mathematical	—	Finite Set.Elem setOf HahnSeries.coeff AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Set.Finite.subset isPWO_iUnion_support Set.Finite.biUnion' Finset.finite_toSet smul_support_finite HahnSeries.isPWO_support Finset.exists_ne_zero_of_sum_ne_zero Set.iUnion_congr_Prop left_ne_zero_of_smul right_ne_zero_of_smul Finset.mem_vaddAntidiagonal
hsum_add 📖	mathematical	—	hsum HahnSeries.SummableFamily instAdd HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid HahnSeries.instAdd	—	HahnSeries.ext finsum_add_distrib finite_co_support
hsum_embDomain 📖	mathematical	—	hsum embDomain	—	HahnSeries.ext dite_apply finsum_emb_domain
hsum_equiv 📖	mathematical	—	hsum Equiv	—	HahnSeries.ext finsum_eq_of_bijective Equiv.bijective
hsum_leadingCoeff_of_le 📖	mathematical	WithTop.some HahnSeries.orderTop AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe HahnSeries.SummableFamily HahnSeries instFunLike Preorder.toLE PartialOrder.toPreorder HahnSeries.coeff	HahnSeries.leadingCoeff hsum	—	hsum_orderTop_of_le HahnSeries.isWF_support HahnSeries.orderTop.eq_1 HahnSeries.orderTop_ne_top HahnSeries.leadingCoeff_of_ne_zero HahnSeries.support_nonempty_iff HahnSeries.untop_orderTop_of_ne_zero finsum_eq_single
hsum_mul 📖	mathematical	—	hsum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring mul HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid HahnSeries.instMul	—	smul_eq_mul instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid mul_eq_smul smul_hsum
hsum_ofFinsupp 📖	mathematical	—	hsum ofFinsupp Finsupp.sum HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid HahnSeries.instZero HahnSeries.instAddCommMonoid	—	HahnSeries.ext Finset.sum_congr map_sum AddMonoidHom.instAddMonoidHomClass finsum_eq_sum_of_support_subset Mathlib.Tactic.Contrapose.contrapose₃
hsum_orderTop_of_le 📖	mathematical	WithTop.some HahnSeries.orderTop AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe HahnSeries.SummableFamily HahnSeries instFunLike Preorder.toLE PartialOrder.toPreorder HahnSeries.coeff	hsum	—	HahnSeries.orderTop_eq_of_le ne_of_eq_of_ne coeff_hsum finsum_eq_single HahnSeries.coeff_orderTop_ne le_hsum_support_mem
hsum_single 📖	mathematical	—	hsum single	—	HahnSeries.ext coeff_hsum finsum_eq_single Pi.single_eq_of_ne single_toFun Pi.single_eq_same
hsum_smul 📖	mathematical	—	hsum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring HahnSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass HahnSeries.SummableFamily instSMul_1 MulZeroClass.toSMulWithZero AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddCommMonoid.toAddMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass HahnSeries.instMul	—	instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid hsum_smul_module HahnSeries.of_symm_smul_of_eq_mul
hsum_smulFamily 📖	mathematical	—	HahnSeries.coeff AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid hsum smulFamily finsum SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass DFunLike.coe HahnSeries.SummableFamily HahnSeries instFunLike	—	—
hsum_smul_module 📖	mathematical	—	hsum HahnSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring HahnSeries.SummableFamily instSMul_1 NonUnitalNonAssocSemiring.toAddCommMonoid MulActionWithZero.toSMulWithZero Semiring.toMonoidWithZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Module.toMulActionWithZero DFunLike.coe Equiv HahnModule SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction EquivLike.toFunLike Equiv.instEquivLike Equiv.symm HahnModule.of HahnModule.instSMul	—	Finite.of_fintype smul_eq hsum_equiv smul_hsum hsum_unique const_toFun
hsum_sub 📖	mathematical	—	hsum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing HahnSeries.SummableFamily instSub Ring.toAddCommGroup HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid HahnSeries.instSub AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup	—	instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid lsum_apply map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
hsum_unique 📖	mathematical	—	hsum DFunLike.coe HahnSeries.SummableFamily HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike Unique.instInhabited	—	HahnSeries.ext finsum_unique
hsum_zero 📖	mathematical	—	hsum HahnSeries.SummableFamily instZero HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid HahnSeries.instZero	—	HahnSeries.ext finsum_zero
isPWO_iUnion_support 📖	mathematical	—	Set.IsPWO PartialOrder.toPreorder Set.iUnion HahnSeries.support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe HahnSeries.SummableFamily HahnSeries instFunLike	—	isPWO_iUnion_support'
isPWO_iUnion_support' 📖	mathematical	—	Set.IsPWO PartialOrder.toPreorder Set.iUnion HahnSeries.support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid toFun	—	—
isPWO_iUnion_support_powers 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid HahnSeries.order MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Set.IsPWO Set.iUnion HahnSeries.support HahnSeries Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero HahnSeries.instSemiring	—	Set.IsPWO.mono Set.IsPWO.addSubmonoid_closure le_trans HahnSeries.order_le_of_coeff_ne_zero Function.mem_support HahnSeries.isPWO_support' Set.iUnion_subset support_pow_subset_closure
isPWO_iUnion_support_prod_mul 📖	—	Set.IsPWO PartialOrder.toPreorder Set.iUnion HahnSeries.support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—	isPWO_iUnion_support_prod_smul instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid
isPWO_iUnion_support_prod_smul 📖	—	Set.IsPWO PartialOrder.toPreorder Set.iUnion HahnSeries.support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—	Set.IsPWO.mono Set.IsPWO.vadd IsOrderedCancelVAdd.toIsOrderedVAdd Set.Subset.trans HahnSeries.isPWO_support Mathlib.Tactic.Contrapose.contrapose₁ HahnSeries.mem_support HahnModule.coeff_smul Finset.sum_empty Finset.support_vaddAntidiagonal_subset_vadd Set.iUnion_mono Set.vadd_subset_vadd Set.subset_iUnion_of_subset
le_hsum_support_mem 📖	—	Preorder.toLE PartialOrder.toPreorder Set Set.instMembership HahnSeries.support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid hsum	—	—	Finset.exists_ne_zero_of_sum_ne_zero coeff_hsum_eq_sum HahnSeries.mem_support
lsum_apply 📖	mathematical	—	DFunLike.coe LinearMap HahnSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring HahnSeries.instSemiring RingHom.id HahnSeries.instNonAssocSemiring HahnSeries.SummableFamily NonUnitalNonAssocSemiring.toAddCommMonoid instAddCommMonoid HahnSeries.instAddCommMonoid instModule AddMonoid.toAddAction AddCommMonoid.toAddMonoid instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid Semiring.toModule LinearMap.instFunLike lsum hsum	—	instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid
mul_eq_smul 📖	mathematical	—	mul smul NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulZeroClass.toSMulWithZero NonUnitalNonAssocSemiring.toMulZeroClass AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddCommMonoid.toAddMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid	—	—
mul_toFun 📖	mathematical	—	DFunLike.coe HahnSeries.SummableFamily NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike mul HahnSeries.instMul	—	—
neg_apply 📖	mathematical	—	DFunLike.coe HahnSeries.SummableFamily AddCommGroup.toAddCommMonoid HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike instNeg HahnSeries.instNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
one_sub_self_mul_hsum_powers 📖	mathematical	WithTop Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithTop.zero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid HahnSeries.orderTop MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	HahnSeries NonUnitalNonAssocSemiring.toAddCommMonoid HahnSeries.instMul HahnSeries.instSub AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup HahnSeries.instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing hsum powers	—	instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid hsum_smul sub_smul one_smul hsum_sub Nat.succ_injective hsum_embDomain embDomain_succ_smul_powers hsum_ofFinsupp Finsupp.sum_single_index sub_sub_cancel
pow_finite_co_support 📖	mathematical	WithTop Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithTop.zero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid HahnSeries.orderTop MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	Set.Finite setOf HahnSeries.coeff	—	isPWO_iUnion_support_powers HahnSeries.zero_le_orderTop_iff le_of_lt Set.Finite.subset Set.finite_singleton co_support_zero Set.WellFoundedOn.induction Set.IsPWO.isWF HahnSeries.isPWO_support Set.Finite.union Set.Finite.image Set.Finite.biUnion Finset.finite_toSet Finset.mem_addAntidiagonal Finset.mem_coe lt_add_of_pos_left IsRightCancelAdd.addRightStrictMono_of_addRightMono IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid lt_of_lt_of_le HahnSeries.zero_lt_orderTop_iff HahnSeries.order_le_of_coeff_ne_zero Function.mem_support Set.mem_union_right Set.mem_singleton HahnSeries.support_mul_subset Set.mem_union_left Set.mem_iUnion add_comm Set.finite_empty
powers_of_not_orderTop_pos 📖	mathematical	WithTop Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithTop.zero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid HahnSeries.orderTop MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	powers single NonUnitalNonAssocSemiring.toAddCommMonoid HahnSeries HahnSeries.instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	ext HahnSeries.ext eq_or_ne pow_zero HahnSeries.coeff_one Pi.single_eq_same zero_pow Pi.single_eq_of_ne
powers_of_orderTop_pos 📖	mathematical	WithTop Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithTop.zero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid HahnSeries.orderTop MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	DFunLike.coe HahnSeries.SummableFamily NonUnitalNonAssocSemiring.toAddCommMonoid HahnSeries instFunLike powers Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero HahnSeries.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring	—	—
powers_toFun 📖	mathematical	—	DFunLike.coe HahnSeries.SummableFamily SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike powers MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero HahnSeries.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring WithTop Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder WithTop.zero HahnSeries.orderTop WithTop.decidableLT LinearOrder.toDecidableLT HahnSeries.instZero	—	—
powers_zero 📖	mathematical	—	powers HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing HahnSeries.instZero single NonUnitalNonAssocSemiring.toAddCommMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid HahnSeries.instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	ext HahnSeries.ext powers_of_orderTop_pos HahnSeries.orderTop_zero eq_or_ne pow_zero HahnSeries.coeff_one Pi.single_eq_same zero_pow Pi.single_eq_of_ne
single_toFun 📖	mathematical	—	DFunLike.coe HahnSeries.SummableFamily HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike single Pi.single HahnSeries.instZero	—	—
smulFamily_toFun 📖	mathematical	—	DFunLike.coe HahnSeries.SummableFamily HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike smulFamily HahnSeries.instSMul SMulWithZero.toSMulZeroClass	—	—
smul_apply 📖	mathematical	—	DFunLike.coe HahnSeries.SummableFamily HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike instSMul_1 Equiv HahnModule SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass EquivLike.toFunLike Equiv.instEquivLike Equiv.symm HahnModule.of HahnModule.instSMul	—	—
smul_apply' 📖	mathematical	—	DFunLike.coe HahnSeries.SummableFamily HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike instSMul HahnSeries.instSMul	—	—
smul_eq 📖	mathematical	—	HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid HahnSeries.SummableFamily instSMul_1 Equiv Equiv.punitProd smul const Finite.of_fintype PUnit.fintype	—	—
smul_hsum 📖	mathematical	—	hsum smul NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulActionWithZero.toSMulWithZero Semiring.toMonoidWithZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Module.toMulActionWithZero DFunLike.coe Equiv HahnModule SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction HahnSeries EquivLike.toFunLike Equiv.instEquivLike Equiv.symm HahnModule.of HahnModule.instSMul	—	HahnSeries.ext isPWO_iUnion_support coeff_smul HahnSeries.isPWO_support HahnModule.coeff_smul Equiv.symm_apply_apply Finset.sum_of_injOn Finset.exists_ne_zero_of_sum_ne_zero coeff_hsum_eq_sum finite_co_support finsum_zero smul_eq_zero_of_left Set.image_id' smul_zero
smul_support_finite 📖	mathematical	—	Set.Finite Function.support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass HahnSeries.coeff DFunLike.coe HahnSeries.SummableFamily HahnSeries instFunLike	—	Set.Finite.subset Set.Finite.prod finite_co_support' Set.toFinite Finite.of_fintype smul_support_subset_prod
smul_support_subset_prod 📖	mathematical	—	Set Set.instHasSubset Function.support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass HahnSeries.coeff DFunLike.coe HahnSeries.SummableFamily HahnSeries instFunLike SetLike.coe Finset Finset.instSetLike Set.Finite.toFinset SProd.sprod Set.instSProd setOf toFun Set.Finite.prod finite_co_support'	—	Set.Finite.prod finite_co_support' Set.Finite.coe_toFinset left_ne_zero_of_smul right_ne_zero_of_smul
smul_toFun 📖	mathematical	—	DFunLike.coe HahnSeries.SummableFamily HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike smul Equiv HahnModule SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass EquivLike.toFunLike Equiv.instEquivLike Equiv.symm HahnModule.of HahnModule.instSMul	—	—
sub_apply 📖	mathematical	—	DFunLike.coe HahnSeries.SummableFamily AddCommGroup.toAddCommMonoid HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike instSub HahnSeries.instSub AddCommGroup.toAddGroup	—	—
sum_vAddAntidiagonal_eq 📖	mathematical	—	Finset.sum Finset.VAddAntidiagonal Function.support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid HahnSeries.coeff DFunLike.coe HahnSeries.SummableFamily HahnSeries instFunLike HahnSeries.isPWO_support' SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass Set.iUnion HahnSeries.support toFun isPWO_iUnion_support'	—	Finset.sum_subset HahnSeries.isPWO_support' isPWO_iUnion_support' smul_eq_zero_of_left smul_zero
support_hsum_subset 📖	mathematical	—	Set Set.instHasSubset HahnSeries.support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid hsum Set.iUnion DFunLike.coe HahnSeries.SummableFamily HahnSeries instFunLike	—	finite_co_support Finset.exists_ne_zero_of_sum_ne_zero finsum_eq_sum coeff_hsum HahnSeries.mem_support Set.mem_iUnion
support_pow_subset_closure 📖	mathematical	—	Set Set.instHasSubset HahnSeries.support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring HahnSeries Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero HahnSeries.instSemiring SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.instSetLike AddSubmonoid.closure	—	pow_zero HahnSeries.coeff_one AddSubmonoid.zero_mem HahnSeries.support_mul_subset SetLike.mem_coe AddSubmonoid.add_mem AddSubmonoid.subset_closure
zero_apply 📖	mathematical	—	DFunLike.coe HahnSeries.SummableFamily HahnSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike instZero HahnSeries.instZero	—	—

(root)

Definitions

Name	Category	Theorems
Summable 📖	MathDef	250 math math: ZLattice.summable_norm_zpow, ArithmeticFunction.vonMangoldt.summable_residueClass_non_primes_div, NNReal.summable_coe, summable_sigma_of_nonneg, ZLattice.summable_norm_sub_inv_pow, NormedSpace.expSeries_summable_of_mem_ball, summable_riemannZetaSummand, Real.summable_ofDigitsTerm, summable_nat_add_iff, Summable.map_iff_of_leftInverse, summable_matrix_transpose, summable_congr, Real.summable_one_div_nat_add_rpow, ENNReal.summable_toNNReal_of_tsum_ne_top, summable_star_iff, FormalMultilinearSeries.changeOriginSeries_summable_aux₃, Real.summable_one_div_int_pow, summable_norm_mul_geometric_of_norm_lt_one, MvPowerSeries.WithPiTopology.summable_of_tendsto_order_atTop_nhds_top, NNReal.summable_sigma, summable_mul_prod_iff_summable_mul_sigma_antidiagonal, Set.Finite.summable, summable_congr_atTop, summable_norm_mul_geometric_of_norm_lt_one', NNReal.not_summable_iff_tendsto_nat_atTop, Finset.summable, summable_condensed_iff_of_eventually_nonneg, Real.summable_nat_rpow_inv, NNReal.summable_geometric, HasSummableGeomSeries.summable_geometric_of_norm_lt_one, EisensteinSeries.summable_left_one_div_linear_sub_one_div_linear, Finset.summable_compl_iff, IsEquivalent.summable_iff_nat, EisensteinSeries.e2Summand_summable, NormedSpace.expSeries_summable, Complex.summable_conj, summable_mul_of_bigO_atTop, Real.not_summable_indicator_one_div_natCast, Real.summable_abs_int_rpow, summable_eisSummand, EisensteinSeries.summable_inv_of_isBigO_rpow_inv, not_summable_of_antitone_of_neg, LiouvilleNumber.summable, lp.summable_mul, NormedSpace.norm_expSeries_summable, LSeries.summable_real_of_abscissaOfAbsConv_lt, summable_unop, summable_const_div_iff, SummableLocallyUniformlyOn.summable, memℓp_gen_iff, EisensteinSeries.summable_of_isBigO_rpow_norm, summable_matrix_diagonal, summable_schlomilch_iff_of_nonneg, RCLike.summable_ofReal, EisensteinSeries.summable_norm_eisSummand, summable_int_iff_summable_nat_and_neg_add_zero, Summable_cotTerm, summable_jacobiTheta₂_term_fderiv_iff, EisensteinSeries.linear_right_summable, EisensteinSeries.summable_linear_left_mul_linear_left, NormedSpace.norm_expSeries_summable_of_mem_ball', PowerSeries.WithPiTopology.summable_prod_of_tendsto_order_atTop_nhds_top, summable_of_ratio_test_tendsto_lt_one, Function.Surjective.summable_iff_of_hasSum_iff, Equiv.summable_iff_of_support, LiouvilleNumber.remainder_summable, Orthonormal.inner_products_summable, ENNReal.summable, Nat.Partition.summable_genFun_term, Summable.of_finite, summable_iff_vanishing_norm, ArithmeticFunction.vonMangoldt.not_summable_residueClass_prime_div, summable_matrix_conjTranspose, NormedSpace.expSeries_summable', NormedSpace.norm_expSeries_summable_of_mem_ball, summable_prod_mul_pow, RCLike.summable_conj, Nat.Primes.not_summable_one_div, summable_int_iff_summable_nat_and_neg, summable_div_const_iff, Real.summable_nat_pow_inv, ZLattice.summable_norm_rpow, FormalMultilinearSeries.not_summable_norm_of_radius_lt_nnnorm, PiCountable.dist_summable, Real.summable_exp_neg_nat, MvPowerSeries.WithPiTopology.summable_pow_of_constantCoeff_eq_zero, PeriodPair.summable_weierstrassPSummand, DirichletCharacter.summable_neg_log_one_sub_mul_prime_cpow, summable_matrix_blockDiagonal', EisensteinSeries.linear_left_summable, summable_powerSeries_of_norm_lt_one, summable_choose_mul_geometric_of_norm_lt_one, Complex.summable_ofReal, summable_pnat_iff_summable_succ, EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_geometric, summable_pow_div_add, NormedSpace.expSeries_div_summable, summable_descFactorial_mul_geometric_of_norm_lt_one, OrthogonalFamily.summable_of_lp, NNReal.summable_nat_add_iff, EisensteinSeries.summable_one_div_norm_rpow, summable_dirichletSummand, EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric, HurwitzKernelBounds.summable_f_nat, summable_of_ratio_norm_eventually_le, MvPowerSeries.WithPiTopology.summable_prod_of_tendsto_weightedOrder_atTop_nhds_top, summable_powerSeries_of_norm_lt, not_summable_indicator_mod_of_antitone_of_neg, NNReal.summable_of_sum_range_le, HasSum.summable, Real.summable_one_div_nat_rpow, ZLattice.summable_norm_pow_inv, NormedSpace.norm_expSeries_summable', summable_abs_iff, NormedSpace.norm_expSeries_div_summable_of_mem_ball, Pi.summable, Real.summable_exp_nat_mul_of_ge, summable_one_div_pow_of_le, Quaternion.summable_coe, summable_iff_not_tendsto_nat_atTop_of_nonneg, summable_norm_pow_mul_geometric_div_one_sub, lp.summable_inner, summable_iff_vanishing, NormedSpace.expSeries_div_summable_of_mem_ball, ENNReal.tsum_coe_ne_top_iff_summable_coe, EisensteinSeries.summable_linear_sub_mul_linear_add, summable_mul_left_iff, FormalMultilinearSeries.changeOriginSeries_summable_aux₁, ModularForm.summable_logDeriv_one_sub_eta_q, summable_const_iff, Function.Injective.summable_iff, ZLattice.summable_norm_sub_rpow, summable_geometric_of_abs_lt_one, Topology.IsInducing.summable_iff_tsum_comp_mem_range, Real.summable_pow_div_factorial, ENNReal.tsum_coe_ne_top_iff_summable, Equiv.summable_iff, summable_condensed_iff_of_nonneg, Real.not_summable_one_div_natCast, NNReal.summable_one_div_rpow, summable_subtype_and_compl, FormalMultilinearSeries.changeOriginSeries_summable_aux₂, IsEquivalent.summable_iff, Real.summable_pow_mul_exp_neg_nat_mul, MvPowerSeries.WithPiTopology.summable_prod_of_tendsto_order_atTop_nhds_top, EisensteinSeries.summable_e2Summand_symmetricIcc, MvPowerSeries.WithPiTopology.summable_iff_summable_coeff, Nat.Partition.summable_genFun_term', ENNReal.tsum_coe_eq_top_iff_not_summable_coe, ENNReal.summable_toReal, summable_of_ne_finset_zero, summable_indicator_mod_iff_summable, summable_geometric_iff_norm_lt_one, summable_zero, summable_pow_mul_geometric_of_norm_lt_one, summable_of_absolute_convergence_real, NNReal.summable_rpow_inv, summable_of_sum_le, summable_iff_cauchySeq_finset, Complex.summable_one_div_nat_cpow, summable_iff_tsum_vanishing, summable_prod_eisSummand, Nat.Primes.summable_rpow, summable_bot, Real.not_summable_natCast_inv, SummableLocallyUniformly.summable, FormalMultilinearSeries.summable_nnnorm_mul_pow, Set.Finite.summable_compl_iff, HilbertBasis.summable_inner_mul_inner, summable_iff_cauchySeq_finset_and_tsum_mem, ZLattice.summable_norm_sub_zpow, summable_subtype_iff_indicator, NNReal.summable_mk, summable_norm_iff, ContinuousLinearEquiv.summable, Metric.exists_subseq_summable_dist_of_cauchySeq, NonarchimedeanAddGroup.summable_iff_tendsto_cofinite_zero, not_summable_iff_tendsto_nat_atTop_of_nonneg, not_summable_of_ratio_norm_eventually_ge, SummableUniformlyOn.summable, summable_of_sum_range_le, NNReal.summable_schlomilch_iff, summable_cotTerm, summable_norm_geometric_of_norm_lt_one, summable_geometric_two', Memℓp.summable, summable_op, summable_empty, NNReal.summable_iff_not_tendsto_nat_atTop, NormedSpace.norm_expSeries_div_summable, summable_pow_mul_jacobiTheta₂_term_bound, summable_bernoulli_fourier, not_summable_one_div_on_primes, EisensteinSeries.summable_e2Summand_symmetricIco, summable_geometric_two, FormalMultilinearSeries.radius_eq_top_iff_summable_norm, Real.summable_one_div_nat_pow, EisensteinSeries.summable_right_one_div_linear_sub_one_div_linear_succ, EisensteinSeries.summable_linear_right_add_one_mul_linear_right, summable_geometric_of_norm_lt_one, FormalMultilinearSeries.summable_norm_mul_pow, summable_star_iff', summable_norm_pow_mul_geometric_of_norm_lt_one, NNReal.summable_condensed_iff, summable_iff_summable_compl_and_tsum_mem, summable_neg_iff, summable_geometric_of_lt_one, summable_mul_right_iff, SummableUniformly.summable, MeasureTheory.integrable_count_iff, PeriodPair.summable_weierstrassPExceptSummand, Summable.map_iff_of_equiv, FormalMultilinearSeries.summable, FormalMultilinearSeries.summable_norm_apply, summable_of_sum_range_norm_le, NormedSpace.expSeries_summable_of_mem_ball', PowerSeries.WithPiTopology.summable_of_tendsto_order_atTop_nhds_top, tsum_def, ModularForm.summable_eta_q, summable_extend_zero, summable_pow_mul_cexp, summable_congr_cofinite, summable_mul_of_bigO_atTop', OrthogonalFamily.summable_iff_norm_sq_summable, summable_partition, summable_jacobiTheta₂'_term_iff, MeasureTheory.summable_measure_toReal, Real.summable_nat_rpow, Real.summable_exp_nat_mul_iff, not_summable_of_ratio_test_tendsto_gt_one, PowerSeries.WithPiTopology.summable_pow_of_constantCoeff_eq_zero, summable_prod_of_nonneg, Summable.of_subsingleton_cod, Real.summable_one_div_int_add_rpow, summable_iff_nat_tsum_vanishing, summable_matrix_blockDiagonal, PowerSeries.WithPiTopology.summable_iff_summable_coeff, summable_geometric_two_encode, MeasureTheory.hasFiniteIntegral_count_iff, summable_jacobiTheta₂_term_iff, HurwitzKernelBounds.summable_f_int, MvPowerSeries.WithPiTopology.summable_of_tendsto_weightedOrder_atTop_nhds_top, NNReal.summable_rpow, Cardinal.summable_cantor_function, lp.tsum_mul_le_mul_norm, summable_of_finite_support, FormalMultilinearSeries.comp_summable_nnreal, summable_indicator_mod_iff, summable_pnat_iff_summable_nat, NonarchimedeanAddGroup.summable_of_tendsto_cofinite_zero

---

← Back to Index