PiTopology

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

Statistics

Metric	Count
Definitions instTopologicalSpace, instUniformSpace	2
Theorems continuous_C, continuous_coeff, continuous_constantCoeff, denseRange_toPowerSeries, hasSum_iff_hasSum_coeff, instCompleteSpace, instIsTopologicalRing, instIsTopologicalSemiring, instIsUniformAddGroup, instT0Space, instT2Space, isTopologicallyNilpotent_iff_constantCoeff_isNilpotent, isTopologicallyNilpotent_of_constantCoeff_isNilpotent, isTopologicallyNilpotent_of_constantCoeff_zero, multipliable_one_add_of_tendsto_order_atTop_nhds_top, multipliable_one_sub_X_pow, one_sub_mul_tsum_pow_of_constantCoeff_eq_zero, summable_iff_summable_coeff, summable_of_tendsto_order_atTop_nhds_top, summable_pow_of_constantCoeff_eq_zero, summable_prod_of_tendsto_order_atTop_nhds_top, tendsto_iff_coeff_tendsto, tendsto_trunc_atTop, tprod_one_sub_X_pow_ne_zero, tsum_pow_mul_one_sub_of_constantCoeff_eq_zero, uniformContinuous_coeff, as_tsum, hasSum_of_monomials_self	28
Total	30

PowerSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
as_tsum 📖	mathematical	—	tsum PowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring WithPiTopology.instTopologicalSpace DFunLike.coe LinearMap RingHom.id Semiring.toModule instModule LinearMap.instFunLike monomial coeff SummationFilter.unconditional	—	HasSum.tsum_eq WithPiTopology.instT2Space SummationFilter.instNeBotUnconditional hasSum_of_monomials_self
hasSum_of_monomials_self 📖	mathematical	—	HasSum PowerSeries instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring WithPiTopology.instTopologicalSpace DFunLike.coe LinearMap RingHom.id Semiring.toModule instModule LinearMap.instFunLike monomial coeff SummationFilter.unconditional	—	RingHomInvPair.ids Equiv.hasSum_iff Finsupp.unique_ext Finsupp.single_eq_same MvPowerSeries.WithPiTopology.hasSum_of_monomials_self

PowerSeries.WithPiTopology

Definitions

Name	Category	Theorems
instTopologicalSpace 📖	CompOp	38 math math: hasSum_iff_hasSum_coeff, continuous_coeff, continuous_constantCoeff, tendsto_iff_coeff_tendsto, instT2Space, PowerSeries.hasSum_of_monomials_self, Nat.Partition.hasProd_powerSeriesMk_card_countRestricted, summable_prod_of_tendsto_order_atTop_nhds_top, Nat.Partition.summable_genFun_term, instIsTopologicalSemiring, Nat.Partition.powerSeriesMk_card_restricted_eq_tprod, denseRange_toPowerSeries, isTopologicallyNilpotent_iff_constantCoeff_isNilpotent, one_sub_mul_tsum_pow_of_constantCoeff_eq_zero, Nat.Partition.hasProd_powerSeriesMk_card_restricted, continuous_C, PowerSeries.as_tsum, Nat.Partition.powerSeriesMk_card_countRestricted_eq_tprod, tsum_pow_mul_one_sub_of_constantCoeff_eq_zero, instIsTopologicalRing, Nat.Partition.summable_genFun_term', Nat.Partition.multipliable_powerSeriesMk_card_restricted, PowerSeries.continuous_aeval, PowerSeries.continuous_eval₂, isTopologicallyNilpotent_of_constantCoeff_isNilpotent, Nat.Partition.hasProd_genFun, multipliable_one_add_of_tendsto_order_atTop_nhds_top, tendsto_trunc_atTop, instT0Space, Nat.Partition.multipliable_powerSeriesMk_card_countRestricted, multipliable_one_sub_X_pow, summable_of_tendsto_order_atTop_nhds_top, isTopologicallyNilpotent_of_constantCoeff_zero, PowerSeries.HasEval.X, Nat.Partition.multipliable_genFun, summable_pow_of_constantCoeff_eq_zero, Nat.Partition.genFun_eq_tprod, summable_iff_summable_coeff
instUniformSpace 📖	CompOp	4 math math: uniformContinuous_coeff, instIsUniformAddGroup, PowerSeries.uniformContinuous_eval₂, instCompleteSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_C 📖	mathematical	—	Continuous PowerSeries instTopologicalSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring PowerSeries.instSemiring RingHom.instFunLike PowerSeries.C	—	MvPowerSeries.WithPiTopology.continuous_C
continuous_coeff 📖	mathematical	—	Continuous PowerSeries instTopologicalSpace DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring PowerSeries.instModule Semiring.toModule LinearMap.instFunLike PowerSeries.coeff	—	continuous_pi_iff continuous_id
continuous_constantCoeff 📖	mathematical	—	Continuous PowerSeries instTopologicalSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring PowerSeries.instSemiring RingHom.instFunLike PowerSeries.constantCoeff	—	continuous_coeff PowerSeries.coeff_zero_eq_constantCoeff
denseRange_toPowerSeries 📖	mathematical	—	DenseRange PowerSeries instTopologicalSpace Polynomial CommSemiring.toSemiring Polynomial.toPowerSeries	—	mem_closure_of_tendsto Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_trunc_atTop Filter.Eventually.of_forall Set.mem_range_self
hasSum_iff_hasSum_coeff 📖	mathematical	—	HasSum PowerSeries PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instTopologicalSpace SummationFilter.unconditional DFunLike.coe LinearMap RingHom.id PowerSeries.instModule Semiring.toModule LinearMap.instFunLike PowerSeries.coeff	—	Finset.sum_congr DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass tendsto_iff_coeff_tendsto
instCompleteSpace 📖	mathematical	—	CompleteSpace PowerSeries instUniformSpace	—	MvPowerSeries.WithPiTopology.instCompleteSpace
instIsTopologicalRing 📖	mathematical	—	IsTopologicalRing PowerSeries instTopologicalSpace NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing PowerSeries.instRing	—	MvPowerSeries.WithPiTopology.instIsTopologicalRing
instIsTopologicalSemiring 📖	mathematical	—	IsTopologicalSemiring PowerSeries instTopologicalSpace NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring PowerSeries.instSemiring	—	MvPowerSeries.WithPiTopology.instIsTopologicalSemiring
instIsUniformAddGroup 📖	mathematical	—	IsUniformAddGroup PowerSeries instUniformSpace PowerSeries.instAddGroup	—	MvPowerSeries.WithPiTopology.instIsUniformAddGroup
instT0Space 📖	mathematical	—	T0Space PowerSeries instTopologicalSpace	—	MvPowerSeries.WithPiTopology.instT0Space
instT2Space 📖	mathematical	—	T2Space PowerSeries instTopologicalSpace	—	MvPowerSeries.WithPiTopology.instT2Space
isTopologicallyNilpotent_iff_constantCoeff_isNilpotent 📖	mathematical	—	Filter.Tendsto PowerSeries Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero PowerSeries.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring Filter.atTop Nat.instPreorder nhds instTopologicalSpace PowerSeries.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsNilpotent DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike PowerSeries.constantCoeff	—	MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_iff_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 PowerSeries PowerSeries.instSemiring RingHom.instFunLike PowerSeries.constantCoeff	Filter.Tendsto Filter.atTop Nat.instPreorder nhds instTopologicalSpace PowerSeries.instZero	—	MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_isNilpotent
isTopologicallyNilpotent_of_constantCoeff_zero 📖	mathematical	DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring PowerSeries.instSemiring CommSemiring.toSemiring RingHom.instFunLike PowerSeries.constantCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	Filter.Tendsto Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Filter.atTop Nat.instPreorder nhds instTopologicalSpace PowerSeries.instZero	—	MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_zero
multipliable_one_add_of_tendsto_order_atTop_nhds_top 📖	mathematical	Filter.Tendsto ENat PowerSeries.order CommSemiring.toSemiring Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds ENat.instTopologicalSpace Top.top instTopENat	Multipliable PowerSeries CommSemiring.toCommMonoid PowerSeries.instCommSemiring instTopologicalSpace Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring PowerSeries.instSemiring MvPowerSeries.instOne SummationFilter.unconditional	—	multipliable_one_add_of_summable_prod summable_prod_of_tendsto_order_atTop_nhds_top
multipliable_one_sub_X_pow 📖	mathematical	—	Multipliable PowerSeries CommRing.toCommMonoid PowerSeries.instCommRing instTopologicalSpace SubNegMonoid.toSub AddGroup.toSubNegMonoid PowerSeries.instAddGroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing MvPowerSeries.instOne CommSemiring.toSemiring CommRing.toCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero PowerSeries.instSemiring PowerSeries.X SummationFilter.unconditional	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim PowerSeries.instSubsingleton sub_eq_add_neg multipliable_one_add_of_tendsto_order_atTop_nhds_top ENat.tendsto_nhds_top_iff_natCast_lt Filter.eventually_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat PowerSeries.order_neg PowerSeries.order_X_pow IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass
one_sub_mul_tsum_pow_of_constantCoeff_eq_zero 📖	mathematical	DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring PowerSeries.instSemiring Ring.toSemiring RingHom.instFunLike PowerSeries.constantCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	MvPowerSeries.instMul SubNegMonoid.toSub AddGroup.toSubNegMonoid PowerSeries.instAddGroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne MvPowerSeries.instOne tsum PowerSeries.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 PowerSeries PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instTopologicalSpace SummationFilter.unconditional DFunLike.coe LinearMap RingHom.id PowerSeries.instModule Semiring.toModule LinearMap.instFunLike PowerSeries.coeff	—	—
summable_of_tendsto_order_atTop_nhds_top 📖	mathematical	Filter.Tendsto ENat PowerSeries.order Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds ENat.instTopologicalSpace Top.top instTopENat	Summable PowerSeries PowerSeries.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₂ PowerSeries.coeff_of_lt_order LT.lt.le
summable_pow_of_constantCoeff_eq_zero 📖	mathematical	DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring PowerSeries.instSemiring RingHom.instFunLike PowerSeries.constantCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	Summable PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instTopologicalSpace Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero SummationFilter.unconditional	—	MvPowerSeries.WithPiTopology.summable_pow_of_constantCoeff_eq_zero
summable_prod_of_tendsto_order_atTop_nhds_top 📖	mathematical	Filter.Tendsto ENat PowerSeries.order CommSemiring.toSemiring Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds ENat.instTopologicalSpace Top.top instTopENat	Summable PowerSeries Finset PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instTopologicalSpace Finset.prod CommSemiring.toCommMonoid PowerSeries.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 PowerSeries.coeff_of_lt_order LT.lt.trans_le not_lt Set.mem_Iio le_trans Finset.single_le_sum IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid PowerSeries.le_order_prod Finset.coe_powerset Finset.coe_Iio
tendsto_iff_coeff_tendsto 📖	mathematical	—	Filter.Tendsto PowerSeries nhds instTopologicalSpace DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring PowerSeries.instModule Semiring.toModule LinearMap.instFunLike PowerSeries.coeff	—	MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto Equiv.forall_congr RingHomInvPair.ids Finsupp.unique_ext Finsupp.single_eq_same
tendsto_trunc_atTop 📖	mathematical	—	Filter.Tendsto PowerSeries Polynomial.toPowerSeries CommSemiring.toSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring PowerSeries.instModule Semiring.toModule Polynomial.module LinearMap.instFunLike PowerSeries.trunc Filter.atTop Nat.instPreorder nhds instTopologicalSpace	—	tendsto_iff_coeff_tendsto tendsto_atTop_of_eventually_const Polynomial.coeff_coe PowerSeries.coeff_trunc
tprod_one_sub_X_pow_ne_zero 📖	—	—	—	—	PowerSeries.coeff_zero_eq_constantCoeff Multipliable.map_tprod SummationFilter.instNeBotUnconditional multipliable_one_sub_X_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass continuous_constantCoeff map_sub RingHomClass.toAddMonoidHomClass map_pow PowerSeries.constantCoeff_X zero_pow sub_zero tprod_one NeZero.one PowerSeries.ext_iff
tsum_pow_mul_one_sub_of_constantCoeff_eq_zero 📖	mathematical	DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring PowerSeries.instSemiring Ring.toSemiring RingHom.instFunLike PowerSeries.constantCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	MvPowerSeries.instMul tsum PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instTopologicalSpace Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero SummationFilter.unconditional SubNegMonoid.toSub AddGroup.toSubNegMonoid PowerSeries.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 PowerSeries instUniformSpace DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring PowerSeries.instModule Semiring.toModule LinearMap.instFunLike PowerSeries.coeff	—	uniformContinuous_pi uniformContinuous_id

---

← Back to Index