Commit 2024-05-16 21:29 579d5472

feat (RingTheory/HahnSeries/Basic): define orderTop, taking values in WithTop (#11965) The existing function HahnSeries.order requires the value type Γ to have Zero as the target of a junk value when the Hahn series vanishes. This is okay for Laurent series, but fails for shifted Laurent series (which often appear in vertex algebras, and also formal expansions of solutions of Fuchsian diff. eqs at regular singular points). This PR introduces an order function that doesn't require Zero, but takes values in WithTop Γ. It is essentially the underlying function of HahnSeries.addVal, but without several additional assumptions on the value and coefficient types. We add some basic API for dealing with WithTop.