Lie derivative of the product of a function and a form If $V$ is a vector field and $\alpha$ is a linear form,
$$ L_V\alpha: X\mapsto V(\alpha(X))-\alpha([V,X]) $$
for every field $X$, is $\mathbb R$-linear, which is trivial since $V$ is a field and $\alpha$ is linear, and $[V,\cdot]$ is also linear. (Is this right?) Also, $L_V:\mathfrak X^*\to\mathfrak X^*$,$ \alpha\mapsto L_V\alpha$ is $\mathbb R$-linear, but I would like to prove that
$$ L_V(f\alpha) = V(f)\alpha+ fL_V\alpha, $$
which is like a Leibniz property.
Any help?
 A: First of all, $[V, \cdot]$ is $\mathbb{R}$-linear but not $C^{\infty}(M)$-linear. That is, $[V, kW] = k[V, W]$ if $k$ is a constant, but for a non-constant function $f$, $[V, fW] \neq f[V, W]$.

Your description of $L_V\alpha$ is via its action on vector fields, so to deduce something about $L_V(f\alpha)$, you should consider how it acts on a vector field. Replacing $\alpha$ by $f\alpha$ in your formula, we obtain
$$(L_V(f\alpha))(X) = V((f\alpha)(X)) - f\alpha([V, X]).$$
Now, $f$ is a function and $\alpha$ is a one-form, so $f\alpha$ is a one-form which satisfies $(f\alpha)(X) = f\alpha(X)$; as $\alpha$ is a one-form and $X$ is a vector field, $\alpha(X)$ is a smooth function, so the right side of this equality is the product of two smooth functions, $f$ and $\alpha(X)$. Now use the fact that $V$ is a vector field, so it is a derivation of smooth functions (in particular, it satisfies the Leibniz rule).
A: I find $\alpha$ a little clumsy so instead of using Greek letters for covectors I will use capital letters with bars, just as vectors are capital letters. 
Indeed, vector fields are derivations mapping scalar fields to scalar fields; and given two such fields there is a function-composition $U \circ V$ which works out to also be a derivation for the commutator/Lie bracket $[U, V] = U \circ V - V \circ U.$ With type-overloading we can define $L_U V = [U, V]$ for vectors and $L_U f = U f$ for scalars, with $L_U (V f) = U (V f)$ straightforwardly, but the reverse (scalar multiplication, not function application) is going to be $L_U(f\cdot V) x = [U, f\cdot V] x$ which by the Leibniz property of $U$ is going to be $U f \cdot V x + f \cdot U (V x) - f \cdot V(U x),$ so $L_U(f \cdot V) = L_U f \cdot V + f \cdot L_U V.$
Now you are introducing another type overload, onto covectors: $$L_U \bar V = U \circ \bar V - \bar V \circ L_U.$$(1) Yes, you are correct to infer that $L_U \bar V$ is a covector, and it is for the linearity reason that you gave.
(2) If you want to know what this does to the one-form $f\cdot\bar V$ the best way to go is to apply the resulting one-form to an actual vector. For, you know that this is $$L_U (f\cdot \bar V)~X = U ((f \cdot \bar V) X) - (f \cdot \bar V) L_UX.$$The former term is $U(f\cdot \bar V X) = U f \cdot \bar V X + f\cdot U(\bar V X)$ while the latter term is $-f\cdot \bar V(L_U X),$ so we get straightforwardly $$L_U(f \cdot \bar V) X = U f \cdot \bar V X + f \cdot \big(U(\bar V X) - \bar V (L_U X)\big) = Uf \cdot \bar V X + f\cdot (L_U \bar V~ X).$$
