Commit 2024-03-15 17:24 e21671e7
View on Github →feat(RingTheory/HahnSeries/Basic): Make a Hahn series from a function with support bounded below (#9574)
Given a locally finite linearly ordered set Γ and a function f on Γ whose support is bounded below, we produce a Hahn series whose coefficients are given by f. We introduce a theorem (borrowing from mathlib3 #18604) for translating the vanishing condition to the partially well-ordered support condition that is used in the definition of Hahn Series.