Commit 2024-10-17 13:07 0c022ea1

View on Github →

feat (RingTheory/HahnSeries) : coefficient-wise map (#16164) This PR introduces HahnSeries.map which applies a zero-preserving map to each coefficient. We more or less copy the Polynomial.map API.

Estimated changes

Modified Mathlib/RingTheory/HahnSeries/Addition.lean

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

modified def HahnSeries.iterateEquiv

added def HahnSeries.map

modified def HahnSeries.ofIterate

modified def HahnSeries.toIterate

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

added theorem HahnSeries.map_C

Modified Mathlib/RingTheory/HahnSeries/PowerSeries.lean