Theorem PowerSeries.monomial_eq_C_mul_X_pow

Modification history

2025-11-19 16:14
Mathlib/RingTheory/PowerSeries/Trunc.lean
feat: power series over a noetherian ring is noetherian (#31149) …
Added PowerSeries.monomial_eq_C_mul_X_powView on Github →