hasseDeriv_zero'

Mathlib.Algebra.Polynomial.HasseDeriv

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

← MathLib Explorer

English

Let R be a semiring and f ∈ R[X]. Then the zero-th Hasse derivative of f equals f.

Русский

Пусть R — полукольцо и f ∈ R[X]. Тогда нулевое производное Хассе от f равно f.

LaTeX

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

Lean4

theorem hasseDeriv_zero' : hasseDeriv 0 f = f := by
  simp only [hasseDeriv_apply, tsub_zero, Nat.choose_zero_right, Nat.cast_one, one_mul, sum_monomial_eq]

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

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

Разделы

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

Аффилиация

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