toLaurent_C_mul_X_pow — Mathlib

English

More generally, toLaurent (C r · X^n) equals C r · T^n, i.e., the image of a monomial with coefficient r and degree n is the Laurant monomial with the same coefficient and exponent n.

Русский

Более обобщённо, toLaurent (C r · X^n) = C r · T^n.

LaTeX

$$$toLaurent (Polynomial.C\\, r * X ^ n) = C\\, r * T\\, n$$$

Lean4

theorem _root_.Polynomial.toLaurent_C_mul_X_pow (n : ℕ) (r : R) : toLaurent (Polynomial.C r * X ^ n) = C r * T n := by
  simp only [map_mul, Polynomial.toLaurent_C, Polynomial.toLaurent_X_pow]

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