hasseDeriv_natDegree_eq_C — Mathlib

English

The Hasse derivative at the natDegree of f equals the constant term C(f.leadingCoeff).

Русский

Производная Хассе на natDegree(f) равна константному полиному C(leadingCoeff(f)).

LaTeX

$$$\mathrm{hasseDeriv}_{f.natDegree} f = C( f.leadingCoeff )$$$

Lean4

theorem hasseDeriv_natDegree_eq_C : f.hasseDeriv f.natDegree = C f.leadingCoeff :=
  by
  have : _ ≤ 0 := Nat.sub_self f.natDegree ▸ natDegree_hasseDeriv_le ..
  rw [eq_C_of_natDegree_le_zero this, hasseDeriv_coeff, zero_add, Nat.choose_self, Nat.cast_one, one_mul, leadingCoeff]

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