hasseDeriv_one

Mathlib.Algebra.Polynomial.HasseDeriv

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

English

The first Hasse derivative coincides with the ordinary derivative as linear maps.

Русский

Первая производная Хассе совпадает с обычной производной как линейные отображения.

LaTeX

$$$\mathrm{hasseDeriv}_1 = \operatorname{derivative}$$$

Lean4

@[simp]
theorem hasseDeriv_one : @hasseDeriv R _ 1 = derivative :=
  LinearMap.ext <| hasseDeriv_one'

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

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

Разделы

Аффилиация

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