algebraMap_X_pow — Mathlib

English

The image of X^n under the canonical algebra map from Polynomial(R) to LaurentPolynomial(R) is the Laurent monomial T^n.

Русский

Образ X^n под каноническим отображением алгебры из Polynomial(R) в LaurentPolynomial(R) равен моному T^n.

LaTeX

$$$\\mathrm{algebraMap}_{R[X] \\to R[T;T^{-1}]}(X^n) = T^n$.$$

Lean4

theorem algebraMap_X_pow (n : ℕ) : algebraMap R[X] R[T;T⁻¹] (X ^ n) = T n :=
  Polynomial.toLaurent_X_pow n

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