coe_add_linearMap — Mathlib

English

The generalized Leibniz rule for Lie derivatives gives an expression for the n-th iterate of a LieDerivation on a bracket, as a sum over antidiagonal indices involving brackets of iterates on a and b.

Русский

Общее правило Лейбница для производной по Ли даёт выражение для n-й итерации на скобке, как сумма по антидиагоналям коэффициентов бинома и скобок итератов на a и b.

LaTeX

$$$D^{[n]} [a,b] = \sum_{ij \in \text{antidiagonal } n} {n \choose i} [D^{[i]} a, D^{[j]} b]$$$

Lean4

@[simp]
theorem coe_add_linearMap (D1 D2 : LieDerivation R L M) : ↑(D1 + D2) = (D1 + D2 : L →ₗ[R] M) :=
  rfl

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