δAux_monomial — Mathlib

English

The action of δAux on a monomial n r in the polynomial ring equals the tensor product of the monomial with the differential of coefficients, realized as (n.prod (Q.val · ^ ·)) ⊗ₜ D R S r.

Русский

Действие δAux на мономе n r в кольце многочленов равно тензорному произведению монома на дифференциал коэффициентов: (n.prod (Q.val · ^ ·)) ⊗ₜ D R S r.

LaTeX

$$$$ \deltaAux\,R\,Q(\mathrm{monomial}\, n\, r) = (n.\mathrm{prod}(Q.\mathrm{val} \cdot ^ \cdot)) \otimes_D D_{R,S} r. $$$$

Lean4

theorem δAux_monomial (n r) : δAux R Q (monomial n r) = (n.prod (Q.val · ^ ·)) ⊗ₜ D R S r :=
  Finsupp.lsum_single _ _ _ _

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