Commit 2025-08-08 20:01 8623f65b
View on Github →refactor (RingTheory/HahnSeries/HEval): remove positive order condition from definition (#25830)
This PR removes the positive order condition for substitution (or Hahn evaluation) of a Hahn series into a power series. When the order is not positive, the function substitutes zero. We also add short lemmas for substitution into PowerSeries.X and PowerSeries.C.