命題
K を標数 0 の可換体とする。
E を K 上の有限次元線型空間とする。
E^* を E の双対空間とする。

v を E の元、
f_1, ..., f_p を E^* の元とする。

i(v)(f_1Λ...Λf_p) = Σ(-1)^(i+1) i(v)f_i(f_1Λ...(f_i)^...Λf_p)

となる。
ここで、(f_i)^ は f_i を省くことを意味する。

証明
x_1, ..., x_p を E の元とする。

i(x_1)(f_1Λ...Λf_p)(x_2, ..., x_p)
= (f_1Λ...Λf_p)(x_1, ..., x_p)
= det(f_i(x_j)) ← 過去スレ014の691
= Σ(-1)^(i+1) f_i(x1)(f_1Λ...(f_i)^...Λf_p)(x_2, ..., x_p) ← 第１列で展開

v = x_1 とおくと

i(v)(f_1Λ...Λf_p) = Σ(-1)^(i+1) i(v)f_i(f_1Λ...(f_i)^...Λf_p)
証明終