eq_C_of_derivative_eq_zero

Mathlib.Algebra.Polynomial.Derivative

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

← MathLib Explorer

English

If derivative f = 0, then f = C (f(0)).

Русский

Если производная f равна нулю, то f = C(f(0)).

LaTeX

$$$f = C\left(f(0)\right)$ if $\operatorname{derivative}(f) = 0$$$

Lean4

theorem eq_C_of_derivative_eq_zero [NoZeroSMulDivisors ℕ R] {f : R[X]} (h : derivative f = 0) : f = C (f.coeff 0) :=
  eq_C_of_natDegree_eq_zero <| natDegree_eq_zero_of_derivative_eq_zero h

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

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

Разделы

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

Аффилиация

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