card_support_C_mul_X_pow_le_one

Mathlib.Algebra.Polynomial.Degree.Support

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

← MathLib Explorer

English

The support of C c · X^n has at most one element, i.e., its cardinality is ≤ 1.

Русский

Поддержка C c · X^n содержит не более одного элемента.

LaTeX

$$$\#\operatorname{supp}(C(c) \cdot X^{n}) \le 1.$$$

Lean4

theorem card_support_C_mul_X_pow_le_one {c : R} {n : ℕ} : #(support (C c * X ^ n)) ≤ 1 :=
  by
  rw [← card_singleton n]
  apply card_le_card (support_C_mul_X_pow' n c)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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