coeffs_X_mul

Mathlib.Algebra.MvPolynomial.Basic

URI: https://scilib.ai/kg/mathlib#MvPolynomial.coeffs_X_mul

English

Similarly, multiplying on the left by X n leaves the coefficient set unchanged.

Русский

Аналогично, умножение слева на X_n не изменяет коэффициентов.

LaTeX

$$$ (X(n) * p).\\mathrm{coeffs} = p.\\mathrm{coeffs}. $$$

Lean4

@[simp]
theorem coeffs_X_mul (p : MvPolynomial σ R) (n : σ) : (X n * p).coeffs = p.coeffs := by
  classical aesop (add simp mem_coeffs_iff)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru