Theorem MvPowerSeries.totalDegree_truncFinset

Modification history

2026-02-23 11:58

Mathlib/RingTheory/MvPowerSeries/Trunc.lean

feat(RingTheory/MvPowerSeries): introduce truncFinset to unify truncations (#35118) …

Added MvPowerSeries.totalDegree_truncFinset View on Github →