Theorem MvPowerSeries.Restricted.coeff_val_mapAdditive

Modification history

2026-09-30 10:15
Mathlib/RingTheory/MvPowerSeries/Restricted.lean
feat: restricted multivariate power series as its own type and some missing API lemmas (#42867) …
Added MvPowerSeries.Restricted.coeff_val_mapAdditiveView on Github →