English
The derivative of a monomial with respect to i is the monomial with the exponent of i decreased by 1 and the coefficient multiplied by the original exponent.
Русский
Производная мономиала по i даёт мономиал с уменьшенным показателем степени i на 1 и коэффициент умножается на исходный показатель степени i.
LaTeX
$$$$ pderiv(i)(monomial(s,a)) = monomial(s - \\{i:1\\}, a \\cdot s(i)). $$$$
Lean4
@[simp]
theorem pderiv_monomial {i : σ} : pderiv i (monomial s a) = monomial (s - single i 1) (a * s i) := by
classical
simp only [pderiv_def, mkDerivation_monomial, Finsupp.smul_sum, smul_eq_mul, ← smul_mul_assoc,
← (monomial _).map_smul]
refine (Finset.sum_eq_single i (fun j _ hne => ?_) fun hi => ?_).trans ?_
· simp [Pi.single_eq_of_ne hne]
· rw [Finsupp.notMem_support_iff] at hi; simp [hi]
· simp
