mem_support_C_mul_X_pow

Mathlib.Algebra.Polynomial.Degree.Support

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

English

If a is in the support of C c · X^n, then a = n.

Русский

Если a ∈ supp(C c · X^n), то a = n.

LaTeX

$$$a \in \operatorname{supp}(C(c) \cdot X^{n}) \Rightarrow a = n.$$$

Lean4

theorem mem_support_C_mul_X_pow {n a : ℕ} {c : R} (h : a ∈ support (C c * X ^ n)) : a = n :=
  mem_singleton.1 <| support_C_mul_X_pow' n c h

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

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

Разделы

Аффилиация

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