Commit 2025-04-07 21:54 d2f6311a

feat: golf, generalize and review API for topological nilpotency of power series (#23683)

• Restate MvPowerSeries.WithPiTopology.tendsto_pow_of_constantCoeff_nilpotent_iff in terms of IsTopologicallyNilpotent, golf its proof, and change its name to MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_iff_of_constantCoeff_isNilpotent
• do the same for some related lemmas, as well as the univariate version
• generalize in the setting of a linearly topologized base ring: in that case, a power series is topologically nilpotent iff its constant coefficient is topologically nilpotent. Notes:
• I could deduce the discrete case from the linear one, but I'm not sure it's worth rethinking the import tree (and in any case we want both statements)
• I didn't add the univariate version of the generalized statement, as the corresponding file doesn't exist in the PowerSeries world, so I'm leaving this as future work if needed.

<!-- The text above the `