support_monomial_subset

Mathlib.Algebra.MvPolynomial.Basic

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

English

The support of X_i is a singleton consisting of the exponent vector with 1 at i and 0 elsewhere.

Русский

Опора X_i — единичное множество с вектором степени, имеющим единицу на i и нули повсюду.

LaTeX

$$$[Nontrivial R] \\\\Rightarrow (X_i).\\\\support = {\\\\, Finsupp.single i 1 \\\\}$$$

Lean4

theorem support_monomial_subset : (monomial s a).support ⊆ { s } :=
  support_single_subset

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

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

Разделы

Аффилиация

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