coeff_monomial_of_ne

Mathlib.Algebra.Polynomial.Basic

URI: https://scilib.ai/kg/mathlib#Polynomial.coeff_monomial_of_ne

English

If m ≠ n, the coefficient of monomial(n, c) at index m is 0.

Русский

Если m ≠ n, коэффициент монома (n, c) на позиции m равен 0.

LaTeX

$$$ \\operatorname{coeff}(\\operatorname{monomial}(n, c))(m) = 0 \\quad \\text{ if } m \\neq n $$$

Lean4

theorem coeff_monomial_of_ne {m n : ℕ} (c : R) (h : m ≠ n) : (monomial n c).coeff m = 0 :=
  Finsupp.single_eq_of_ne h

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

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

Разделы

Аффилиация

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