Theorem MvPowerSeries.truncFinset_one

Modification history

2026-02-23 11:58

Mathlib/RingTheory/MvPowerSeries/Trunc.lean

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

Added MvPowerSeries.truncFinset_one View on Github →