Commit 2025-01-24 14:15 33cc4f3c

View on Github →

feat(Topology/Algebra/TopologicallyNilpotent): top nilpotent in linear topologies (#20971) In a monoid with zero and a topology, an element is topologically nilpotent if its powers converge to zero. In a ring with a linear topology, sum and product of (commuting) topologically nilpotent elements are topologically nilpotent.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Ideal/Basic.lean

added theorem Ideal.add_pow_add_pred_mem_of_pow_mem_of_commute

added theorem Ideal.add_pow_mem_of_pow_mem_of_le_of_commute

Modified Mathlib/RingTheory/Ideal/Defs.lean

Created Mathlib/Topology/Algebra/TopologicallyNilpotent.lean

added theorem IsTopologicallyNilpotent.add

added theorem IsTopologicallyNilpotent.add_of_commute

added theorem IsTopologicallyNilpotent.exists_pow_mem_of_mem_nhds

added theorem IsTopologicallyNilpotent.map

added theorem IsTopologicallyNilpotent.mul_left

added theorem IsTopologicallyNilpotent.mul_left_of_commute

added theorem IsTopologicallyNilpotent.mul_right

added theorem IsTopologicallyNilpotent.mul_right_of_commute

added theorem IsTopologicallyNilpotent.zero

added def IsTopologicallyNilpotent