Theorem PowerSeries.WithPiTopology.tprod_one_sub_X_pow_ne_zero

Modification history

2025-12-05 16:31
Mathlib/RingTheory/PowerSeries/PiTopology.lean
feat(Combinatorics): Glaisher's theorem (#30618) …
Added PowerSeries.WithPiTopology.tprod_one_sub_X_pow_ne_zeroView on Github →