Commit 2025-04-04 15:36 d7375dd3

View on Github →

feat(RingTheory/MvPowerSeries/Substitution) : better API for rescale (#23642) This redefines MvPowerSeries.rescale under commutative semirings, to keep in line with PowerSeries.rescale.

Estimated changes

Modified Mathlib/RingTheory/MvPowerSeries/Substitution.lean

added theorem MvPowerSeries.HasSubst.add

added theorem MvPowerSeries.HasSubst.mul_left

added theorem MvPowerSeries.HasSubst.mul_right

added theorem MvPowerSeries.HasSubst.smul

added theorem MvPowerSeries.HasSubst.smul_X

added theorem MvPowerSeries.HasSubst.zero

deleted theorem MvPowerSeries.coe_rescale_algHom

modified theorem MvPowerSeries.coeff_rescale

deleted theorem MvPowerSeries.hasSubst_X

deleted theorem MvPowerSeries.hasSubst_add

deleted theorem MvPowerSeries.hasSubst_mul

deleted theorem MvPowerSeries.hasSubst_rescale

deleted theorem MvPowerSeries.hasSubst_smul

deleted theorem MvPowerSeries.hasSubst_zero

added theorem MvPowerSeries.rescaleAlgHom_apply

added theorem MvPowerSeries.rescaleAlgHom_mul

added theorem MvPowerSeries.rescaleAlgHom_one

deleted theorem MvPowerSeries.rescale_algHom_comp

deleted theorem MvPowerSeries.rescale_algHom_one

added theorem MvPowerSeries.rescale_homogeneous_eq_smul

deleted theorem MvPowerSeries.rescale_linear_eq_smul

added theorem MvPowerSeries.rescale_mul

modified theorem MvPowerSeries.rescale_one

added theorem MvPowerSeries.rescale_rescale

deleted theorem MvPowerSeries.rescale_rescale_apply

added theorem MvPowerSeries.rescale_zero

added theorem MvPowerSeries.subst_self

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

modified theorem PowerSeries.rescale_zero_apply