Theorem Ideal.add_pow_mem_of_pow_mem_of_le_of_commute

Modification history

2025-01-24 14:15
Mathlib/RingTheory/Ideal/Basic.lean
feat(Topology/Algebra/TopologicallyNilpotent): top nilpotent in linear topologies (#20971) …
Added Ideal.add_pow_mem_of_pow_mem_of_le_of_commuteView on Github →