PiTopology

📁 Source: Mathlib/RingTheory/MvPowerSeries/PiTopology.lean

Statistics

Metric	Count
Definitions instTopologicalSpace, instUniformSpace	2
Theorems as_tsum, continuous_C, continuous_coeff, continuous_constantCoeff, denseRange_toMvPowerSeries, hasSum_iff_hasSum_coeff, hasSum_of_monomials_self, instCompleteSpace, instContinuousSMul, instIsTopologicalRing, instIsTopologicalSemiring, instIsUniformAddGroup, instT0Space, instT2Space, instTopologicalSpace_mono, isTopologicallyNilpotent_iff_constantCoeff_isNilpotent, isTopologicallyNilpotent_of_constantCoeff_isNilpotent, isTopologicallyNilpotent_of_constantCoeff_zero, multipliable_one_add_of_tendsto_order_atTop_nhds_top, multipliable_one_add_of_tendsto_weightedOrder_atTop_nhds_top, one_sub_mul_tsum_pow_of_constantCoeff_eq_zero, summable_iff_summable_coeff, summable_of_tendsto_order_atTop_nhds_top, summable_of_tendsto_weightedOrder_atTop_nhds_top, summable_pow_of_constantCoeff_eq_zero, summable_prod_of_tendsto_order_atTop_nhds_top, summable_prod_of_tendsto_weightedOrder_atTop_nhds_top, tendsto_iff_coeff_tendsto, tendsto_trunc'_atTop, tendsto_trunc_atTop, tsum_pow_mul_one_sub_of_constantCoeff_eq_zero, uniformContinuous_coeff, variables_tendsto_zero	33
Total	35

MvPowerSeries.WithPiTopology

Definitions

Name	Category	Theorems
instTopologicalSpace 📖	CompOp	50 math math: tendsto_trunc_atTop, instIsTopologicalRing, MvPowerSeries.eval₂Hom_eq_extend, isTopologicallyNilpotent_iff_constantCoeff_isNilpotent, summable_of_tendsto_order_atTop_nhds_top, MvPowerSeries.continuous_aeval, multipliable_one_add_of_tendsto_order_atTop_nhds_top, MvPowerSeries.continuous_eval₂, instContinuousSMul, continuous_coeff, MvPowerSeries.LinearTopology.isTopologicallyNilpotent_iff_constantCoeff, as_tsum, MvPowerSeries.LinearTopology.instIsLinearTopologyMulOpposite, hasSum_iff_hasSum_coeff, MvPowerSeries.LinearTopology.isTopologicallyNilpotent_of_constantCoeff, summable_pow_of_constantCoeff_eq_zero, MvPowerSeries.continuous_subst, MvPolynomial.toMvPowerSeries_isDenseInducing, instT2Space, MvPowerSeries.comp_subst_apply, one_sub_mul_tsum_pow_of_constantCoeff_eq_zero, MvPowerSeries.hasSubst_iff_hasEval_of_discreteTopology, MvPowerSeries.LinearTopology.instIsLinearTopologyOfMulOpposite, summable_prod_of_tendsto_weightedOrder_atTop_nhds_top, tsum_pow_mul_one_sub_of_constantCoeff_eq_zero, MvPowerSeries.coeff_zero_iff, hasSum_of_monomials_self, denseRange_toMvPowerSeries, PowerSeries.HasSubst.hasEval, summable_prod_of_tendsto_order_atTop_nhds_top, summable_iff_summable_coeff, MvPowerSeries.HasEval.X, tendsto_trunc'_atTop, isTopologicallyNilpotent_of_constantCoeff_isNilpotent, MvPowerSeries.comp_subst, instTopologicalSpace_mono, isTopologicallyNilpotent_of_constantCoeff_zero, MvPowerSeries.HasSubst.hasEval, instIsTopologicalSemiring, variables_tendsto_zero, instT0Space, tendsto_iff_coeff_tendsto, MvPowerSeries.comp_substAlgHom, PowerSeries.hasSubst_iff_hasEval_of_discreteTopology, continuous_constantCoeff, MvPowerSeries.aeval_unique, MvPowerSeries.LinearTopology.hasBasis_nhds_zero, summable_of_tendsto_weightedOrder_atTop_nhds_top, continuous_C, multipliable_one_add_of_tendsto_weightedOrder_atTop_nhds_top
instUniformSpace 📖	CompOp	8 math math: MvPowerSeries.subst_eq_eval₂, MvPolynomial.toMvPowerSeries_isUniformInducing, MvPowerSeries.substAlgHom_eq_aeval, uniformContinuous_coeff, instIsUniformAddGroup, MvPowerSeries.uniformContinuous_eval₂, PowerSeries.substAlgHom_eq_aeval, instCompleteSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
as_tsum 📖	mathematical	—	tsum MvPowerSeries Finsupp MulZeroClass.toZero Nat.instMulZeroClass MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instTopologicalSpace DFunLike.coe LinearMap RingHom.id Semiring.toModule MvPowerSeries.instModule LinearMap.instFunLike MvPowerSeries.monomial MvPowerSeries.coeff SummationFilter.unconditional	—	HasSum.tsum_eq instT2Space SummationFilter.instNeBotUnconditional hasSum_of_monomials_self
continuous_C 📖	mathematical	—	Continuous MvPowerSeries instTopologicalSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring MvPowerSeries.instSemiring RingHom.instFunLike MvPowerSeries.C	—	tendsto_iff_coeff_tendsto MvPowerSeries.coeff_C Filter.tendsto_id tendsto_const_nhds
continuous_coeff 📖	mathematical	—	Continuous MvPowerSeries instTopologicalSpace DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring MvPowerSeries.instModule Semiring.toModule LinearMap.instFunLike MvPowerSeries.coeff	—	continuous_pi_iff continuous_id
continuous_constantCoeff 📖	mathematical	—	Continuous MvPowerSeries instTopologicalSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring MvPowerSeries.instSemiring RingHom.instFunLike MvPowerSeries.constantCoeff	—	continuous_coeff
denseRange_toMvPowerSeries 📖	mathematical	—	DenseRange MvPowerSeries instTopologicalSpace MvPolynomial MvPolynomial.toMvPowerSeries	—	mem_closure_of_tendsto Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder tendsto_trunc'_atTop Filter.Eventually.of_forall Set.mem_range_self
hasSum_iff_hasSum_coeff 📖	mathematical	—	HasSum MvPowerSeries MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instTopologicalSpace SummationFilter.unconditional DFunLike.coe LinearMap RingHom.id MvPowerSeries.instModule Semiring.toModule LinearMap.instFunLike MvPowerSeries.coeff	—	Finset.sum_congr DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass tendsto_iff_coeff_tendsto
hasSum_of_monomials_self 📖	mathematical	—	HasSum MvPowerSeries Finsupp MulZeroClass.toZero Nat.instMulZeroClass MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instTopologicalSpace DFunLike.coe LinearMap RingHom.id Semiring.toModule MvPowerSeries.instModule LinearMap.instFunLike MvPowerSeries.monomial MvPowerSeries.coeff SummationFilter.unconditional	—	Pi.hasSum MvPowerSeries.coeff_monomial_same hasSum_single MvPowerSeries.coeff_monomial_ne SummationFilter.instLeAtTopUnconditional
instCompleteSpace 📖	mathematical	—	CompleteSpace MvPowerSeries instUniformSpace	—	Pi.complete
instContinuousSMul 📖	mathematical	—	ContinuousSMul MvPowerSeries Algebra.toSMul MvPowerSeries.instSemiring MvPowerSeries.instAlgebra instTopologicalSpace	—	instContinuousSMulForall
instIsTopologicalRing 📖	mathematical	—	IsTopologicalRing MvPowerSeries instTopologicalSpace NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing MvPowerSeries.instRing	—	instIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring continuous_pi Continuous.comp ContinuousNeg.continuous_neg IsSemitopologicalRing.toContinuousNeg IsTopologicalRing.toIsSemitopologicalRing continuous_coeff
instIsTopologicalSemiring 📖	mathematical	—	IsTopologicalSemiring MvPowerSeries instTopologicalSpace NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MvPowerSeries.instSemiring	—	continuous_pi Continuous.comp continuous_add IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring Continuous.prodMk Continuous.fst' continuous_coeff Continuous.snd' continuous_finset_sum continuous_mul IsTopologicalSemiring.toContinuousMul
instIsUniformAddGroup 📖	mathematical	—	IsUniformAddGroup MvPowerSeries instUniformSpace MvPowerSeries.instAddGroup	—	Pi.instIsUniformAddGroup
instT0Space 📖	mathematical	—	T0Space MvPowerSeries instTopologicalSpace	—	Pi.instT0Space
instT2Space 📖	mathematical	—	T2Space MvPowerSeries instTopologicalSpace	—	Pi.t2Space
instTopologicalSpace_mono 📖	mathematical	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder	TopologicalSpace MvPowerSeries Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder instTopologicalSpace	—	le_imp_le_of_le_of_le iInf_mono induced_mono le_refl iInf_le
isTopologicallyNilpotent_iff_constantCoeff_isNilpotent 📖	mathematical	—	IsTopologicallyNilpotent MvPowerSeries Semiring.toMonoidWithZero MvPowerSeries.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring instTopologicalSpace IsNilpotent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toPow MonoidWithZero.toMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike MvPowerSeries.constantCoeff	—	IsTopologicallyNilpotent.map RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass continuous_constantCoeff Filter.Eventually.exists Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat nhds_discrete isTopologicallyNilpotent_of_constantCoeff_isNilpotent
isTopologicallyNilpotent_of_constantCoeff_isNilpotent 📖	mathematical	IsNilpotent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe RingHom MvPowerSeries MvPowerSeries.instSemiring RingHom.instFunLike MvPowerSeries.constantCoeff	IsTopologicallyNilpotent MvPowerSeries Semiring.toMonoidWithZero MvPowerSeries.instSemiring CommSemiring.toSemiring instTopologicalSpace	—	tendsto_atTop_of_eventually_const MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
isTopologicallyNilpotent_of_constantCoeff_zero 📖	mathematical	DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring RingHom.instFunLike MvPowerSeries.constantCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	Filter.Tendsto MvPowerSeries Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MvPowerSeries.instSemiring CommSemiring.toSemiring Filter.atTop Nat.instPreorder nhds instTopologicalSpace MvPowerSeries.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	isTopologicallyNilpotent_of_constantCoeff_isNilpotent IsNilpotent.zero
multipliable_one_add_of_tendsto_order_atTop_nhds_top 📖	mathematical	Filter.Tendsto ENat MvPowerSeries.order CommSemiring.toSemiring Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds ENat.instTopologicalSpace Top.top instTopENat	Multipliable MvPowerSeries CommSemiring.toCommMonoid MvPowerSeries.instCommSemiring instTopologicalSpace Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring MvPowerSeries.instOne SummationFilter.unconditional	—	multipliable_one_add_of_summable_prod summable_prod_of_tendsto_order_atTop_nhds_top
multipliable_one_add_of_tendsto_weightedOrder_atTop_nhds_top 📖	mathematical	Filter.Tendsto ENat MvPowerSeries.weightedOrder CommSemiring.toSemiring Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds ENat.instTopologicalSpace Top.top instTopENat	Multipliable MvPowerSeries CommSemiring.toCommMonoid MvPowerSeries.instCommSemiring instTopologicalSpace Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring MvPowerSeries.instOne SummationFilter.unconditional	—	multipliable_one_add_of_summable_prod summable_prod_of_tendsto_weightedOrder_atTop_nhds_top
one_sub_mul_tsum_pow_of_constantCoeff_eq_zero 📖	mathematical	DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring MvPowerSeries.instSemiring Ring.toSemiring RingHom.instFunLike MvPowerSeries.constantCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	MvPowerSeries MvPowerSeries.instMul Ring.toSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid MvPowerSeries.instAddGroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne MvPowerSeries.instOne tsum MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instTopologicalSpace Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MvPowerSeries.instSemiring SummationFilter.unconditional	—	Summable.one_sub_mul_tsum_pow instIsTopologicalRing instT2Space summable_pow_of_constantCoeff_eq_zero
summable_iff_summable_coeff 📖	mathematical	—	Summable MvPowerSeries MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instTopologicalSpace SummationFilter.unconditional DFunLike.coe LinearMap RingHom.id MvPowerSeries.instModule Semiring.toModule LinearMap.instFunLike MvPowerSeries.coeff	—	—
summable_of_tendsto_order_atTop_nhds_top 📖	mathematical	Filter.Tendsto ENat MvPowerSeries.order Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds ENat.instTopologicalSpace Top.top instTopENat	Summable MvPowerSeries MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instTopologicalSpace SummationFilter.unconditional	—	summable_of_tendsto_weightedOrder_atTop_nhds_top
summable_of_tendsto_weightedOrder_atTop_nhds_top 📖	mathematical	Filter.Tendsto ENat MvPowerSeries.weightedOrder Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds ENat.instTopologicalSpace Top.top instTopENat	Summable MvPowerSeries MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instTopologicalSpace SummationFilter.unconditional	—	isEmpty_or_nonempty summable_empty summable_iff_summable_coeff SemilatticeSup.instIsDirectedOrder summable_of_hasFiniteSupport SummationFilter.instHasSupportOfLeAtTop SummationFilter.instLeAtTopUnconditional Set.Finite.subset Set.finite_Iic Mathlib.Tactic.Contrapose.contrapose₂ MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder LT.lt.le
summable_pow_of_constantCoeff_eq_zero 📖	mathematical	DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring MvPowerSeries.instSemiring RingHom.instFunLike MvPowerSeries.constantCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	Summable MvPowerSeries MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instTopologicalSpace Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MvPowerSeries.instSemiring SummationFilter.unconditional	—	summable_of_tendsto_order_atTop_nhds_top instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat lt_of_lt_of_le LT.lt.trans_le ENat.coe_lt_coe GE.ge.le nsmul_eq_mul ENat.self_le_mul_right MvPowerSeries.order_ne_zero_iff_constCoeff_eq_zero MvPowerSeries.le_order_pow
summable_prod_of_tendsto_order_atTop_nhds_top 📖	mathematical	Filter.Tendsto ENat MvPowerSeries.order CommSemiring.toSemiring Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds ENat.instTopologicalSpace Top.top instTopENat	Summable MvPowerSeries Finset MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instTopologicalSpace Finset.prod CommSemiring.toCommMonoid MvPowerSeries.instCommSemiring SummationFilter.unconditional	—	summable_prod_of_tendsto_weightedOrder_atTop_nhds_top
summable_prod_of_tendsto_weightedOrder_atTop_nhds_top 📖	mathematical	Filter.Tendsto ENat MvPowerSeries.weightedOrder CommSemiring.toSemiring Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds ENat.instTopologicalSpace Top.top instTopENat	Summable MvPowerSeries Finset MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instTopologicalSpace Finset.prod CommSemiring.toCommMonoid MvPowerSeries.instCommSemiring SummationFilter.unconditional	—	isEmpty_or_nonempty Summable.of_finite Finite.of_fintype SummationFilter.instHasSupportOfLeAtTop SummationFilter.instLeAtTopUnconditional summable_iff_summable_coeff summable_of_hasFiniteSupport SemilatticeSup.instIsDirectedOrder Set.Finite.subset Finset.finite_toSet Mathlib.Tactic.Contrapose.contrapose₂ Set.not_subset MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder LT.lt.trans_le not_lt Set.mem_Iio le_trans Finset.single_le_sum IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid MvPowerSeries.le_weightedOrder_prod Finset.coe_powerset Finset.coe_Iio
tendsto_iff_coeff_tendsto 📖	mathematical	—	Filter.Tendsto MvPowerSeries nhds instTopologicalSpace DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring MvPowerSeries.instModule Semiring.toModule LinearMap.instFunLike MvPowerSeries.coeff	—	nhds_pi Filter.tendsto_pi
tendsto_trunc'_atTop 📖	mathematical	—	Filter.Tendsto Finsupp MulZeroClass.toZero Nat.instMulZeroClass MvPowerSeries MvPolynomial.toMvPowerSeries DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid MvPowerSeries.instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike MvPowerSeries.trunc' Filter.atTop Finsupp.preorder Nat.instPreorder nhds instTopologicalSpace	—	tendsto_iff_coeff_tendsto tendsto_atTop_of_eventually_const Nat.instCanonicallyOrderedAdd MvPowerSeries.coeff_trunc'
tendsto_trunc_atTop 📖	mathematical	—	Filter.Tendsto Finsupp MulZeroClass.toZero Nat.instMulZeroClass MvPowerSeries MvPolynomial.toMvPowerSeries DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid MvPowerSeries.instModule Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike MvPowerSeries.trunc Filter.atTop Finsupp.preorder Nat.instPreorder nhds instTopologicalSpace	—	tendsto_iff_coeff_tendsto tendsto_atTop_of_eventually_const MvPolynomial.coeff_coe Nat.instCanonicallyOrderedAdd MvPowerSeries.coeff_trunc lt_of_lt_of_le IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono Finsupp.instIsLeftCancelAdd instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Finsupp.isOrderedAddMonoid Nat.instIsOrderedAddMonoid IsOrderedCancelAddMonoid.toAddLeftReflectLT Finsupp.isOrderedCancelAddMonoid zero_le Finsupp.instCanonicallyOrderedAddOfAddLeftMono Nat.instOrderedSub Finsupp.single_eq_same Nat.instNoMaxOrder
tsum_pow_mul_one_sub_of_constantCoeff_eq_zero 📖	mathematical	DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring MvPowerSeries.instSemiring Ring.toSemiring RingHom.instFunLike MvPowerSeries.constantCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	MvPowerSeries MvPowerSeries.instMul Ring.toSemiring tsum MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instTopologicalSpace Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MvPowerSeries.instSemiring SummationFilter.unconditional SubNegMonoid.toSub AddGroup.toSubNegMonoid MvPowerSeries.instAddGroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne MvPowerSeries.instOne	—	Summable.tsum_pow_mul_one_sub instIsTopologicalRing instT2Space summable_pow_of_constantCoeff_eq_zero
uniformContinuous_coeff 📖	mathematical	—	UniformContinuous MvPowerSeries instUniformSpace DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring MvPowerSeries.instModule Semiring.toModule LinearMap.instFunLike MvPowerSeries.coeff	—	uniformContinuous_pi uniformContinuous_id
variables_tendsto_zero 📖	mathematical	—	Filter.Tendsto MvPowerSeries MvPowerSeries.X Filter.cofinite nhds instTopologicalSpace MvPowerSeries.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	MvPowerSeries.coeff_X tendsto_nhds_of_eventually_eq Filter.mp_mem Filter.eventually_cofinite_ne Filter.univ_mem' Filter.Eventually.of_forall

---

← Back to Index