Support order type of iterated Hahn series #
Flattening an iterated Hahn series orders its support lexicographically, with the outer exponent dominant. Choosing one nonzero inner coefficient over each outer support point therefore embeds the outer support into the flattened support. In particular, flattening cannot decrease the ordinary support order type contributed by the outer series.
theorem
HahnSeries.supportOrderType_outer_le_iterateRingEquiv
{R : Type v}
{Γ Γ' : Type u}
[Semiring R]
[AddCommMonoid Γ]
[LinearOrder Γ]
[IsOrderedCancelAddMonoid Γ]
[AddCommMonoid Γ']
[LinearOrder Γ']
[IsOrderedCancelAddMonoid Γ']
(x : HahnSeries Γ (HahnSeries Γ' R))
:
The outer support order type of an iterated Hahn series is no larger than the support order type of its flattening.