support_X_empty

Mathlib.Algebra.Polynomial.Basic

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

English

If 1 = 0 in the coefficient ring, the polynomial X has empty support.

Русский

Если 1 = 0 в кольце коэффициентов, опора X пустая.

LaTeX

$$$ (X : R[X]).\mathrm{support} = \emptyset \quad \text{if } (1 : R) = 0$$$

Lean4

theorem support_X_empty (H : (1 : R) = 0) : (X : R[X]).support = ∅ := by rw [X, H, monomial_zero_right, support_zero]

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

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

Разделы

Аффилиация

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