coeffList_C

Mathlib.Algebra.Polynomial.CoeffList

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

← MathLib Explorer

English

If x ≠ 0, then the coefficient list of the constant polynomial Cx equals [x].

Русский

Если x ≠ 0, то коэффициентный список константного полинома Cx равен [x].

LaTeX

$$$ (C x).coeffList = [x] $ при x ≠ 0$$

Lean4

@[simp]
theorem coeffList_C {x : R} (h : x ≠ 0) : (C x).coeffList = [x] := by
  simp [coeffList, List.range_succ, degree_eq_natDegree (C_ne_zero.mpr h)]

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

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

Разделы

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

Аффилиация

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