Theorem MvPowerSeries.coeff_truncFinset_mul_truncFinset_eq_coeff_mul

Modification history

2026-02-23 11:58
Mathlib/RingTheory/MvPowerSeries/Trunc.lean
feat(RingTheory/MvPowerSeries): introduce truncFinset to unify truncations (#35118) …
Added MvPowerSeries.coeff_truncFinset_mul_truncFinset_eq_coeff_mulView on Github →