Theorem PowerSeries.expand_subst

Modification history

2026-03-21 06:41

Mathlib/RingTheory/PowerSeries/Expand.lean

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

Modified PowerSeries.expand_subst View on Github →

2026-01-18 13:18

Mathlib/RingTheory/PowerSeries/Expand.lean

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

Added PowerSeries.expand_subst View on Github →