English
For a monomial monomial(n,r), the k-th Hasse derivative is a homogeneous monomial of degree n−k with coefficient binomial(n,k)·r.
Русский
Для монома x^n·r, k-я производная Хассе равна гомогенной моно-мономии степени n−k с коэффициентом \binom{n}{k}·r.
LaTeX
$$$\mathrm{hasseDeriv}_k(\mathrm{monomial}(n,r)) = \mathrm{monomial}(n-k, \binom{n}{k}\, r)$$$
Lean4
@[simp]
theorem hasseDeriv_monomial (n : ℕ) (r : R) : hasseDeriv k (monomial n r) = monomial (n - k) (↑(n.choose k) * r) :=
by
ext i
simp only [hasseDeriv_coeff, coeff_monomial]
by_cases hnik : n = i + k
· grind
· rw [if_neg hnik, mul_zero]
by_cases hkn : k ≤ n
· rw [← tsub_eq_iff_eq_add_of_le hkn] at hnik
rw [if_neg hnik]
· push_neg at hkn
rw [Nat.choose_eq_zero_of_lt hkn, Nat.cast_zero, zero_mul, ite_self]
