implicitDeriv_X

Mathlib.RingTheory.Derivation.MapCoeffs

URI: https://scilib.ai/kg/mathlib#Differential.implicitDeriv_X

English

The implicit derivative applied to X yields the polynomial itself, i.e., implicitDeriv(v) acts as identity on X.

Русский

При X производная через implicitDeriv возвращает сам X, т.е. implicitDeriv(v) действует как тождественное отображение на X.

LaTeX

$$$\text{implicitDeriv}(v)(X) = v$$$

Lean4

@[simp]
theorem implicitDeriv_X (v : A[X]) : implicitDeriv v X = v := by simp [implicitDeriv]

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

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

Разделы

Аффилиация

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