mkDerivationₗ_monomial — Mathlib

English

The linear component of mkDerivation acts on monomials by distributing over the sum of contributions from each index.

Русский

Линейная часть mkDerivation действует на мономе, распределяясь по сумме вклада каждого индекса.

LaTeX

$$$\\\\mathrm{mkDerivation}_{\\ell}(R,f)(\\\\mathrm{monomial}(s,r)) = r \\\\cdot \\\\sum_i (\\\\mathrm{monomial}(s - \\delta_i, r) \\\\cdot f(i))$$$

Lean4

theorem mkDerivationₗ_monomial (f : σ → A) (s : σ →₀ ℕ) (r : R) :
    mkDerivationₗ R f (monomial s r) = r • s.sum fun i k => monomial (s - Finsupp.single i 1) (k : R) • f i :=
  sum_monomial_eq <| LinearMap.map_zero _

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