HahnSeries.ofPowerSeries_X

theorem HahnSeries.ofPowerSeries_X : ∀ {Γ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : StrictOrderedSemiring Γ], (HahnSeries.ofPowerSeries Γ R) PowerSeries.X = (HahnSeries.single 1) 1

The theorem `HahnSeries.ofPowerSeries_X` states that for any types Γ and R, where Γ is a strict ordered semiring and R is a semiring, the application of the function `HahnSeries.ofPowerSeries` onto the power series variable `PowerSeries.X` is equal to the Hahn series which has coefficient 1 at 1 and zero elsewhere, represented as `HahnSeries.single 1 1`. In other words, the power series variable, when casted as a Hahn series with coefficients from a strict ordered semiring, is equivalent to a Hahn series with a single nonzero coefficient 1 at 1.

More concisely: For any strict ordered semiring Γ and semiring R, the Hahn series obtained from casting the power series variable `PowerSeries.X` as a Hahn series with coefficients from Γ is equal to the Hahn series with a single nonzero coefficient 1 at 1.