Commit 2024-02-06 20:37 8fac0fc0

feat: HahnSeries smul order inequality (#9848) Given a Hahn series x and a scalar r such that r • x ≠ 0, the order of r • x is not strictly less than the order of x. If the exponent poset is linearly ordered, the order of x is less than or equal to the order of r • x. (Note that the order of a Hahn series is not uniquely defined when the exponent poset is not linearly ordered.) This is a complement to the addition result HahnSeries.min_order_le_order_add.