hasseDeriv_zero

Mathlib.Algebra.Polynomial.HasseDeriv

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

English

The zero-th Hasse derivative is the identity map on polynomials.

Русский

Нулевое производное Хассе является тождественным отображением на полиномы.

LaTeX

$$$\mathrm{hasseDeriv}_0 = \mathrm{Id}$$$

Lean4

@[simp]
theorem hasseDeriv_zero : @hasseDeriv R _ 0 = LinearMap.id :=
  LinearMap.ext <| hasseDeriv_zero'

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

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

Разделы

Аффилиация

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