English
The composition of Hasse derivatives satisfies hasseDeriv k ∘ hasseDeriv l = binom(k+l, k) · hasseDeriv(k+l).
Русский
Сложение производных Хассе даёт выражение через биномиальные коэффициенты: hasseDeriv_k ∘ hasseDeriv_l = binom(k+l, k) · hasseDeriv_{k+l}.
LaTeX
$$$\mathrm{hasseDeriv}_k \circ \mathrm{hasseDeriv}_l = {k+l \choose k} \, \mathrm{hasseDeriv}_{k+l}$$$
Lean4
theorem hasseDeriv_comp (k l : ℕ) : (@hasseDeriv R _ k).comp (hasseDeriv l) = (k + l).choose k • hasseDeriv (k + l) :=
by
ext i : 2
simp only [LinearMap.smul_apply, comp_apply, LinearMap.coe_comp, smul_monomial, hasseDeriv_apply, mul_one,
monomial_eq_zero_iff, sum_monomial_index, mul_zero, ← tsub_add_eq_tsub_tsub, add_comm l k]
rw_mod_cast [nsmul_eq_mul]
rw [← Nat.cast_mul]
congr 2
by_cases hikl : i < k + l
· rw [choose_eq_zero_of_lt hikl, mul_zero]
by_cases hil : i < l
· rw [choose_eq_zero_of_lt hil, mul_zero]
· push_neg at hil
rw [← tsub_lt_iff_right hil] at hikl
rw [choose_eq_zero_of_lt hikl, zero_mul]
push_neg at hikl
apply @cast_injective ℚ
have h1 : l ≤ i := le_of_add_le_right hikl
have h2 : k ≤ i - l := le_tsub_of_add_le_right hikl
have h3 : k ≤ k + l := le_self_add
push_cast
rw [cast_choose ℚ h1, cast_choose ℚ h2, cast_choose ℚ h3, cast_choose ℚ hikl]
rw [show i - (k + l) = i - l - k by rw [add_comm]; apply tsub_add_eq_tsub_tsub]
simp only [add_tsub_cancel_left]
field_simp
