valuation_X_pow — Mathlib

English

For any integer d, the monomial with exponent -d and coefficient α^{-1} equals the inverse of the monomial with exponent d and coefficient α.

Русский

Для любого целого d моном с показателем -d и коэффициентом α^{-1} равен обратному моному с показателем d и коэффициентом α.

LaTeX

$$$\mathrm{single}(-d)(\alpha)^{-1} = (\mathrm{single}(d)(\alpha))^{-1}$$$

Lean4

theorem valuation_X_pow (s : ℕ) : Valued.v (((X : K⟦X⟧) : K⸨X⸩) ^ s) = exp (-(s : ℤ)) := by
  rw [map_pow, valuation_def, ← LaurentSeries.coe_algebraMap, valuation_of_algebraMap, intValuation_X, ← exp_nsmul,
    smul_neg, nsmul_one]

Похожие утверждения