Commit 2026-03-21 06:41 fedc3c58

View on Github →

feat(MvPowerSeries): subst_C and omit some finiteness of index set (#35842)

Estimated changes

Modified Mathlib/RingTheory/MvPowerSeries/Expand.lean

Modified Mathlib/RingTheory/MvPowerSeries/Substitution.lean

modified theorem MvPowerSeries.map_subst

added theorem MvPowerSeries.subst_C

added theorem MvPowerSeries.subst_sub

Modified Mathlib/RingTheory/PowerSeries/Expand.lean

modified theorem PowerSeries.expand_subst

Modified Mathlib/RingTheory/PowerSeries/Substitution.lean

added theorem PowerSeries.subst_C

added theorem PowerSeries.subst_sub