Commit 2026-01-18 13:18 18ef4ef4

View on Github →

feat(RingTheory/MvPowerSeries): some theorems about expand (#33885)

Estimated changes

Modified Mathlib/RingTheory/MvPowerSeries/Expand.lean

added theorem MvPowerSeries.constantCoeff_expand

added theorem MvPowerSeries.expand_subst

added theorem MvPowerSeries.order_expand

Modified Mathlib/RingTheory/MvPowerSeries/Substitution.lean

added theorem MvPowerSeries.constantCoeff_subst_eq_zero

Modified Mathlib/RingTheory/PowerSeries/Expand.lean

added theorem PowerSeries.coeff_expand

modified theorem PowerSeries.coeff_expand_mul

modified theorem PowerSeries.coeff_expand_of_not_dvd

added theorem PowerSeries.constantCoeff_expand

added theorem PowerSeries.expand_smul

added theorem PowerSeries.expand_subst

added theorem PowerSeries.order_expand

modified theorem PowerSeries.support_expand

modified theorem PowerSeries.support_expand_subset

Modified Mathlib/RingTheory/PowerSeries/Substitution.lean

added theorem PowerSeries.constantCoeff_subst_eq_zero