mkDerivationₗ — Mathlib

English

For a given map f : σ → A, there exists a derivation on the polynomial ring that sends X_i to f(i).

Русский

Для заданной отображения f: σ → A существует производная на кольце многочленов, которая отправляет X_i в f(i).

LaTeX

$$$\\\\exists D : Derivation R (MvPolynomial σ R) A, \\\\forall i, D(X_i) = f(i)$$$

Lean4

/-- The derivation on `MvPolynomial σ R` that takes value `f i` on `X i`, as a linear map.
Use `MvPolynomial.mkDerivation` instead. -/
def mkDerivationₗ (f : σ → A) : MvPolynomial σ R →ₗ[R] A :=
  Finsupp.lsum R fun xs : σ →₀ ℕ =>
    (LinearMap.ringLmapEquivSelf R R A).symm <| xs.sum fun i k => monomial (xs - Finsupp.single i 1) (k : R) • f i

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