Units of the nonpositive Hahn-series ring #
Half of LM24, Fact 2.5.2: the units of the finite-support nonpositive Hahn-series ring are exactly the nonzero constant series.
Finiteness of the support is not used. The order of a nonzero series is the least exponent of its support, so it is at most zero here, and it is additive on products over a domain. A product equal to one therefore forces both orders to vanish, which leaves the whole support at zero.
theorem
HahnSeries.Nonpositive.isUnit_finiteSupport_iff_exists_scalar
{G : Type u}
{K : Type v}
[LinearOrder G]
[AddCommGroup G]
[IsOrderedAddMonoid G]
[Field K]
(p : ↥finiteSupportSubring)
:
LM24, Fact 2.5.2: the units of the finite-support nonpositive Hahn-series ring are exactly the nonzero constant series.