Theorem PowerSeries.support_expand_subset

Modification history

2026-01-18 13:18

Mathlib/RingTheory/PowerSeries/Expand.lean

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

Modified PowerSeries.support_expand_subset View on Github →

2025-12-18 09:08

Mathlib/RingTheory/PowerSeries/Expand.lean

feat(RingTheory/MvPowerSeries): some APIs about `expand` (#33005) …

Added PowerSeries.support_expand_subset View on Github →