Commit 2025-01-30 06:00 e6b6302b
View on Github →feat(RingTheory/HahnSeries): define powerSeriesFamily (#20205) This PR defines a summable family of power series whose elements are non-negative powers of a fixed Hahn series times the coefficients of a formal power series. We will use it to define algebra homomorphisms from rings of formal power series to Hahn series.