Scaled Lie derivative defect identity (source code)

= Scaled Lie derivative defect identity
{title2=$f\mathcal L_X-\mathcal L_{fX}=D_{X\otimes df}$}

For a <smooth function> $f$ and <vector field> $X$,
$$
f\mathcal L_X-\mathcal L_{fX}=D_{X\otimes df}
$$
on every <tensor field>, with $X\otimes df$ interpreted as the <endomorphism> $Y\mapsto Y(f)X$. Both sides vanish on functions; on <vector fields> this follows from $[fX,Y]=f[X,Y]-Y(f)X$. Both are contraction-compatible <tensor derivations>, so agreement on functions and <vector fields> proves equality on all tensor types. In particular $\mathcal L_{fX}\omega=f\mathcal L_X\omega+\omega(X)df$.