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	46 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, 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, instTopologicalSpace_mono, isTopologicallyNilpotent_of_constantCoeff_zero, MvPowerSeries.HasSubst.hasEval, instIsTopologicalSemiring, variables_tendsto_zero, instT0Space, tendsto_iff_coeff_tendsto, PowerSeries.hasSubst_iff_hasEval_of_discreteTopology, continuous_constantCoeff, 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 IsTopologicalRing.toContinuousNeg continuous_coeff
instIsTopologicalSemiring 📖	mathematical	—	IsTopologicalSemiring MvPowerSeries instTopologicalSpace NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MvPowerSeries.instSemiring	—	continuous_pi Continuous.comp continuous_add IsTopologicalSemiring.toContinuousAdd 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	MvPowerSeries 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.toNatPow 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.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe RingHom MvPowerSeries MvPowerSeries.instSemiring RingHom.instFunLike MvPowerSeries.constantCoeff	IsTopologicallyNilpotent 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 Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Filter.atTop Nat.instPreorder nhds instTopologicalSpace MvPowerSeries.instZero	—	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 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 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.instMul SubNegMonoid.toSub AddGroup.toSubNegMonoid MvPowerSeries.instAddGroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne MvPowerSeries.instOne tsum MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instTopologicalSpace Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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_finite_support 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.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instTopologicalSpace Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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 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 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_finite_support 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 AddMonoidHom MvPolynomial AddZeroClass.toAddZero AddMonoid.toAddZeroClass MvPowerSeries.instAddMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring AddMonoidHom.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 AddMonoidHom MvPolynomial AddZeroClass.toAddZero AddMonoid.toAddZeroClass MvPowerSeries.instAddMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring AddMonoidHom.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 AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Finsupp.isOrderedAddMonoid Nat.instIsOrderedAddMonoid IsOrderedCancelAddMonoid.toAddLeftReflectLT Finsupp.isOrderedCancelAddMonoid Nat.instIsOrderedCancelAddMonoid zero_le Finsupp.instCanonicallyOrderedAddOfAddLeftMono Nat.instOrderedSub Finsupp.single_eq_same Nat.instZeroLEOneClass
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.instMul tsum MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instTopologicalSpace Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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