support_X_pow — Mathlib

English

If 1 ≠ 0 in the coefficient ring, then the support of X^n is {n} for every n.

Русский

Если 1 ≠ 0 в кольце коэффициентов, опорой X^n является {n} для каждого n.

LaTeX

$$$ (X^n : R[X]).\mathrm{support} = \{ n \}$ \text{(assuming } 1 \neq 0 \text{ in } R\text{)}$$

Lean4

theorem support_X_pow (H : ¬(1 : R) = 0) (n : ℕ) : (X ^ n : R[X]).support = singleton n :=
  by
  convert support_monomial n H
  exact X_pow_eq_monomial n

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