命題
M を n 次元多様体とする。
X を M 上のベクトル場とし、ω ∈ Ω^p(M) (>>315) とする。

このとき、L_X(ω) = i(X)(dω) + d(i(X)ω)
ただし、p = 0 のとき i(X)ω = 0 とする。

証明
p = 0 のとき、L_X(ω) = Xf であり、i(X)(dω) = df(X) = Xf
よって、L_X(ω) = i(X)(dω)

p ＞ 0 とし、X_1, ..., X_p ∈ X(M) (>>238) とする。
>>347, >>307, >>311より、

i(X)(dω)(X_1, ..., X_p) = dω(X, X_1, ..., X_p)
= X(ω(X_1, ..., X_p))
+ Σ(-1)^(i+2)X_iω(X, X_1, ..., (X_i)^, ..., X_p)
+ Σ[1 ≦ j ≦ p] (-1)^(1+j+1)ω([X, X_j], X^, ..., (X_j)^, ..., X_p)
+ Σ[i ＜ j] (-1)^(i+1+j+1)X_iω([X_i, X_j], X, X_1, ..., (X_i)^, ..., (X_j)^, ..., X_p)
= L_X(ω)(X_1, ..., X_p) - d(i(X)ω)(X_1, ..., X_p)

証明終