Commit 2025-02-19 22:17 9302f151

View on Github →

feat(RingTheory/MvPowerSeries/Trunc): define variant of truncation (#20958) MvPowerSeries.trunc truncates a multivariate power series strictly below some exponent (using Finset.Iio). Define analogously MvPowerSeries.trunc' that truncates using Finset.Iic.

Estimated changes

Modified Mathlib/RingTheory/MvPowerSeries/Trunc.lean

added theorem MvPowerSeries.coeff_mul_eq_coeff_trunc'_mul_trunc'

added theorem MvPowerSeries.coeff_trunc'

added theorem MvPowerSeries.coeff_truncFun'

added def MvPowerSeries.trunc'

added theorem MvPowerSeries.trunc'_C

added theorem MvPowerSeries.trunc'_C_mul

added theorem MvPowerSeries.trunc'_map

added theorem MvPowerSeries.trunc'_one

added def MvPowerSeries.truncFun'

added theorem MvPowerSeries.trunc_C

deleted theorem MvPowerSeries.trunc_c