Commit 2025-02-17 03:56 75f198c9

View on Github →

feat (RingTheory/HahnSeries): algebra homomorphism from PowerSeries to HahnSeries. (#21313) This PR defines the R-algebra homomorphism from PowerSeries R to HahnSeries Γ R that takes X to some positive-order element, and extends formally to infinite sums.

Estimated changes

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

added theorem HahnSeries.orderTop_of_Subsingleton

Modified Mathlib/RingTheory/HahnSeries/HEval.lean

added theorem PowerSeries.coeff_heval

added theorem PowerSeries.coeff_heval_zero

added def PowerSeries.heval

added theorem PowerSeries.heval_mul

added theorem PowerSeries.heval_unit

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

added theorem HahnModule.orderTop_vAdd_le_orderTop_smul

added theorem HahnSeries.orderTop_add_le_mul

added theorem HahnSeries.orderTop_nsmul_le_orderTop_pow