Ssreflect Users Discussion List

[Laurent Théry <>]

> Opps I am wrong this is not so simple, so maybe Cyril solution is a 
> more direct one. 

I thought the function f that I was defining was not linear over the 
whole space but it is

Lemma f_is_linear : linear f.
Proof.
move=> k x y; rewrite /f scaler_sumr -big_split /=.
by apply: eq_bigr=> i _; rewrite linearD linearZ scalerDl scalerA.
Qed.

So it is restriction to V1 is an isomorphism.

--
Laurent