Finitely supported Hahn series #
Mathlib's HahnSeries.ofFinsuppLinearMap views a finitely supported function Γ →₀ V as a Hahn
series. This file records that it sends Finsupp.single a v to the monomial
HahnSeries.single a v, which reduces computations with finitely supported series, such as
polynomial loops, to monomials.
@[simp]
theorem
HahnSeries.ofFinsuppLinearMap_single
{Γ : Type u_1}
{R : Type u_2}
{V : Type u_3}
[PartialOrder Γ]
[Semiring R]
[AddCommMonoid V]
[Module R V]
(a : Γ)
(v : V)
:
A finitely supported function with a single nonzero value is a monomial.