Commit 2026-02-23 11:58 a1e3af18

View on Github →

feat(RingTheory/MvPowerSeries): introduce truncFinset to unify truncations (#35118) Resolves the TODO in MvPowerSeries/Trunc.lean by implementing a general truncation map truncFinset, which paves the way for unifying strict and non-strict truncations and defining other truncations

Estimated changes

Modified Mathlib/Order/Interval/Finset/Basic.lean

added theorem Finset.sup_Iic_of_monotone

Modified Mathlib/RingTheory/MvPowerSeries/Trunc.lean

modified theorem MvPowerSeries.coeff_mul_eq_coeff_trunc'_mul_trunc'

modified theorem MvPowerSeries.coeff_trunc'

added theorem MvPowerSeries.coeff_trunc'_mul_trunc'_eq_coeff_mul

modified theorem MvPowerSeries.coeff_trunc

added theorem MvPowerSeries.coeff_truncFinset

added theorem MvPowerSeries.coeff_truncFinset_eq_zero

added theorem MvPowerSeries.coeff_truncFinset_mul_truncFinset_eq_coeff_mul

added theorem MvPowerSeries.coeff_truncFinset_of_mem

deleted theorem MvPowerSeries.coeff_truncFun'

deleted theorem MvPowerSeries.coeff_truncFun

added theorem MvPowerSeries.support_truncFinset_subset

added theorem MvPowerSeries.totalDegree_truncFinset

modified def MvPowerSeries.trunc'

modified theorem MvPowerSeries.trunc'_C

modified theorem MvPowerSeries.trunc'_one

modified def MvPowerSeries.trunc

added def MvPowerSeries.truncFinset

added theorem MvPowerSeries.truncFinset_C

added theorem MvPowerSeries.truncFinset_apply

added theorem MvPowerSeries.truncFinset_map

added theorem MvPowerSeries.truncFinset_monomial

added theorem MvPowerSeries.truncFinset_monomial_eq_zero

added theorem MvPowerSeries.truncFinset_one

added theorem MvPowerSeries.truncFinset_truncFinset

added theorem MvPowerSeries.truncFinset_truncFinset_pow

deleted def MvPowerSeries.truncFun'

deleted def MvPowerSeries.truncFun