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 MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring WithPiTopology.instTopologicalSpace DFunLike.coe LinearMap RingHom.id Semiring.toModule MvPowerSeries.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 MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring WithPiTopology.instTopologicalSpace DFunLike.coe LinearMap RingHom.id Semiring.toModule MvPowerSeries.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	39 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, PowerSeries.aeval_unique, 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 MvPowerSeries.instSemiring RingHom.instFunLike PowerSeries.C	—	MvPowerSeries.WithPiTopology.continuous_C
continuous_coeff 📖	mathematical	—	Continuous PowerSeries instTopologicalSpace DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring MvPowerSeries.instModule Semiring.toModule LinearMap.instFunLike PowerSeries.coeff	—	continuous_pi_iff continuous_id
continuous_constantCoeff 📖	mathematical	—	Continuous PowerSeries instTopologicalSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring MvPowerSeries.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 MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instTopologicalSpace SummationFilter.unconditional DFunLike.coe LinearMap RingHom.id MvPowerSeries.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 MvPowerSeries.instRing	—	MvPowerSeries.WithPiTopology.instIsTopologicalRing
instIsTopologicalSemiring 📖	mathematical	—	IsTopologicalSemiring PowerSeries instTopologicalSpace NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MvPowerSeries.instSemiring	—	MvPowerSeries.WithPiTopology.instIsTopologicalSemiring
instIsUniformAddGroup 📖	mathematical	—	IsUniformAddGroup PowerSeries instUniformSpace MvPowerSeries.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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MvPowerSeries.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring Filter.atTop Nat.instPreorder nhds instTopologicalSpace MvPowerSeries.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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe RingHom PowerSeries MvPowerSeries.instSemiring RingHom.instFunLike PowerSeries.constantCoeff	Filter.Tendsto PowerSeries 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	—	MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_isNilpotent
isTopologicallyNilpotent_of_constantCoeff_zero 📖	mathematical	DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring MvPowerSeries.instSemiring CommSemiring.toSemiring RingHom.instFunLike PowerSeries.constantCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	Filter.Tendsto PowerSeries 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	—	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 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_sub_X_pow 📖	mathematical	—	Multipliable PowerSeries CommRing.toCommMonoid MvPowerSeries.instCommRing instTopologicalSpace SubNegMonoid.toSub AddGroup.toSubNegMonoid MvPowerSeries.instAddGroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing MvPowerSeries.instOne CommSemiring.toSemiring CommRing.toCommSemiring Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MvPowerSeries.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
one_sub_mul_tsum_pow_of_constantCoeff_eq_zero 📖	mathematical	DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring MvPowerSeries.instSemiring Ring.toSemiring RingHom.instFunLike PowerSeries.constantCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	PowerSeries 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 PowerSeries MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instTopologicalSpace SummationFilter.unconditional DFunLike.coe LinearMap RingHom.id MvPowerSeries.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 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₂ PowerSeries.coeff_of_lt_order LT.lt.le
summable_pow_of_constantCoeff_eq_zero 📖	mathematical	DFunLike.coe RingHom PowerSeries Semiring.toNonAssocSemiring MvPowerSeries.instSemiring RingHom.instFunLike PowerSeries.constantCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	Summable PowerSeries MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instTopologicalSpace Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MvPowerSeries.instSemiring 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 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 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 MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring MvPowerSeries.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 MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring MvPowerSeries.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 MvPowerSeries.instSemiring Ring.toSemiring RingHom.instFunLike PowerSeries.constantCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	PowerSeries 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 PowerSeries instUniformSpace DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring MvPowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring MvPowerSeries.instModule Semiring.toModule LinearMap.instFunLike PowerSeries.coeff	—	uniformContinuous_pi uniformContinuous_id

---

← Back to Index