Documentation Verification Report

TopologicallyNilpotent

📁 Source: Mathlib/Topology/Algebra/TopologicallyNilpotent.lean

Statistics

Metric	Count
Definitions `IsTopologicallyNilpotent`, `topologicalNilradical`	2
Theorems `isTopologicallyNilpotent`, `add`, `add_of_commute`, `exists_pow_mem_of_mem_nhds`, `map`, `mem_topologicalNilradical_iff`, `mul_left`, `mul_left_of_commute`, `mul_right`, `mul_right_of_commute`, `zero`, `coe_topologicalNilradical`	12
Total	14

IsNilpotent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isTopologicallyNilpotent` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Monoid.toNatPow` `MonoidWithZero.toMonoid`	`IsTopologicallyNilpotent`	—	`tendsto_atTop_of_eventually_const` `pow_add` `MulZeroClass.zero_mul`

IsTopologicallyNilpotent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`IsTopologicallyNilpotent` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`add_of_commute` `Commute.all`
`add_of_commute` 📖	mathematical	`IsTopologicallyNilpotent` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Distrib.toAdd`	—	`Filter.HasBasis.tendsto_iff` `Filter.atTop_basis` `IsLinearTopology.hasBasis_ideal` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `exists_pow_mem_of_mem_nhds` `Ideal.add_pow_mem_of_pow_mem_of_le_of_commute` `le_trans`
`exists_pow_mem_of_mem_nhds` 📖	mathematical	`IsTopologicallyNilpotent` `Set` `Filter` `Filter.instMembership` `nhds` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	`Set.instMembership` `Monoid.toNatPow` `MonoidWithZero.toMonoid`	—	`Filter.Eventually.exists` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.Tendsto.eventually_mem`
`map` 📖	—	`Continuous` `DFunLike.coe` `IsTopologicallyNilpotent`	—	—	`MonoidWithZeroHomClass.toMonoidHomClass` `Filter.Tendsto.comp` `Continuous.tendsto` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass`
`mem_topologicalNilradical_iff` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `topologicalNilradical` `IsTopologicallyNilpotent` `Semiring.toMonoidWithZero`	—	`add` `mul_left`
`mul_left` 📖	mathematical	`IsTopologicallyNilpotent` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`mul_left_of_commute` `Commute.all`
`mul_left_of_commute` 📖	—	`IsTopologicallyNilpotent` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—	`Commute.mul_pow` `IsLinearTopology.tendsto_mul_zero_of_right`
`mul_right` 📖	mathematical	`IsTopologicallyNilpotent` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`mul_right_of_commute` `IsLinearTopology.instMulOpposite` `Commute.all`
`mul_right_of_commute` 📖	—	`IsTopologicallyNilpotent` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—	`Commute.mul_pow` `IsLinearTopology.tendsto_mul_zero_of_left`
`zero` 📖	mathematical	—	`IsTopologicallyNilpotent` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`tendsto_atTop_of_eventually_const` `zero_pow`

(root)

Definitions

Name	Category	Theorems
`IsTopologicallyNilpotent` 📖	MathDef	10 math math: `MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_iff_constantCoeff_isNilpotent`, `MvPowerSeries.LinearTopology.isTopologicallyNilpotent_iff_constantCoeff`, `IsNilpotent.isTopologicallyNilpotent`, `coe_topologicalNilradical`, `MvPowerSeries.hasEval_def`, `MvPowerSeries.HasEval.hpow`, `MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_isNilpotent`, `IsTopologicallyNilpotent.mem_topologicalNilradical_iff`, `PowerSeries.hasEval_def`, `IsTopologicallyNilpotent.zero`
`topologicalNilradical` 📖	CompOp	2 math math: `coe_topologicalNilradical`, `IsTopologicallyNilpotent.mem_topologicalNilradical_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_topologicalNilradical` 📖	mathematical	—	`SetLike.coe` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.setLike` `topologicalNilradical` `setOf` `IsTopologicallyNilpotent` `Semiring.toMonoidWithZero`	—	—

---

← Back to Index