nextCoeff_X_add_C

Mathlib.Algebra.Polynomial.Degree.Operations

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

English

For any nontrivial ring S, nextCoeff(X + C c) = c for all c ∈ S.

Русский

Для любого ненульного кольца S nextCoeff(X + C c) = c для всех c ∈ S.

LaTeX

$$$\mathrm{nextCoeff}(X + C c) = c$$$

Lean4

@[simp]
theorem nextCoeff_X_add_C [Semiring S] (c : S) : nextCoeff (X + C c) = c :=
  by
  nontriviality S
  simp [nextCoeff_of_natDegree_pos]

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

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

Разделы

Аффилиация

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