Theorem PowerSeries.coeff_expand_mul

Modification history

2026-01-18 13:18
Mathlib/RingTheory/PowerSeries/Expand.lean
feat(RingTheory/MvPowerSeries): some theorems about expand (#33885)
Modified PowerSeries.coeff_expand_mulView on Github →
2025-12-18 09:08
Mathlib/RingTheory/PowerSeries/Expand.lean
feat(RingTheory/MvPowerSeries): some APIs about `expand` (#33005) …
Added PowerSeries.coeff_expand_mulView on Github →