nextCoeff_C_mul_X_add_C

Mathlib.Algebra.Polynomial.Degree.Lemmas

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

English

If a ≠ 0, then nextCoeff (C a * X + C c) = c.

Русский

Если a ≠ 0, то nextCoeff (C a · X + C c) = c.

LaTeX

$$@[simp] nextCoeff (C a * X + C c) = c$$

Lean4

@[simp]
theorem nextCoeff_C_mul_X_add_C (ha : a ≠ 0) (c : R) : nextCoeff (C a * X + C c) = c := by
  rw [nextCoeff_of_natDegree_pos] <;> simp [ha]

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

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

Разделы

Аффилиация

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