Commit 2026-03-03 20:34 627f637e

View on Github →

feat(RingTheory/PowerSeries/Substitution): add API (#26961)

Estimated changes

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

added theorem PowerSeries.rescale_algebraMap_map

added theorem PowerSeries.rescale_map

Modified Mathlib/RingTheory/PowerSeries/Substitution.lean

deleted theorem MvPowerSeries.rescaleUnit

added theorem PowerSeries.coe_rescaleAlgHom

added theorem PowerSeries.rescale_eq

added theorem PowerSeries.rescale_eq_subst

added theorem PowerSeries.subst_def

added theorem PowerSeries.subst_rescale_of_degree_eq_one