Theorem PowerSeries.coeff_coeToMvPowerSeries

Modification history

2026-06-30 06:44
Mathlib/RingTheory/PowerSeries/Basic.lean
feat(FormalGroup): `F(X,0)=X` and `F(0,X)=X` (#38052) …
Added PowerSeries.coeff_coeToMvPowerSeriesView on Github →