apply_eval_eq

Mathlib.RingTheory.Derivation.MapCoeffs

URI: https://scilib.ai/kg/mathlib#Derivation.apply_eval_eq

← MathLib Explorer

English

For derivations D1, D2, the bracket bracket D1 D2 applied to a is D1(D2(a)) − D2(D1(a)).

Русский

Для производных D1, D2 операция скобки на элемент a даёт D1(D2(a)) − D2(D1(a)).

LaTeX

$$$⁅D_1,D_2⁆(a) = D_1(D_2(a)) - D_2(D_1(a))$$$

Lean4

theorem apply_eval_eq (x : A) (p : A[X]) :
    d (eval x p) = PolynomialModule.eval x (d.mapCoeffs p) + eval x (derivative p) • d x :=
  apply_aeval_eq d x p

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

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

Разделы

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

Аффилиация

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