English
The zpow expression for monomials generalizes the natural and negative exponent cases; monomial with exponent n equals the nth zpow of the unit monomial.
Русский
Выражение zpow для мономов обобщает натуральные и отрицательные показатели: моному при показателе n равна n-ая zpow единичного монома.
LaTeX
$$$\mathrm{single}(n)(1) = 1^{n}$ in zpow sense; for all $n\in\mathbb{Z}$.$$
Lean4
theorem valuation_single_zpow (s : ℤ) : Valued.v (HahnSeries.single s (1 : K) : K⸨X⸩) = exp (-(s : ℤ)) :=
by
obtain s | s := s
· rw [Int.ofNat_eq_coe, ← HahnSeries.ofPowerSeries_X_pow, PowerSeries.coe_pow, valuation_X_pow]
·
rw [Int.negSucc_eq, ← inv_inj, ← map_inv₀, inv_single, neg_neg, ← Int.natCast_succ, inv_one, ←
HahnSeries.ofPowerSeries_X_pow, PowerSeries.coe_pow, valuation_X_pow, exp_neg]
/- The coefficients of a power series vanish in degree strictly less than its valuation. -/
