support_X — Mathlib

English

The support of X raised to a power n is the singleton containing the exponent vector with n at position s.

Русский

Опора X^n имеет вид единичного множества с вектором степени, равным n на позиции s.

LaTeX

$$$[Nontrivial R] (X s)^n: \\operatorname{support} = { Finsupp.single s n }$$$

Lean4

theorem support_X [Nontrivial R] : (X n : MvPolynomial σ R).support = {Finsupp.single n 1} := by
  classical rw [X, support_monomial, if_neg]; exact one_ne_zero

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