C_mul_X_eq_monomial

Mathlib.Algebra.MvPolynomial.Basic

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

English

A monomial with coefficient b is the zero polynomial if and only if b = 0.

Русский

Моном с коэффициентом b равен нулю тогда и только тогда, когда b = 0.

LaTeX

$$$\mathrm{monomial}(s,b) = 0 \iff b = 0$$$

Lean4

theorem C_mul_X_eq_monomial {s : σ} {a : R} : C a * X s = monomial (Finsupp.single s 1) a := by
  rw [← C_mul_X_pow_eq_monomial, pow_one]

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

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

Разделы

Аффилиация

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