Ssreflect Users Discussion List

[Cyril <>]

Hi, I would like to prove that the subspaces generated by the delta_mx form
a direct sum. I expected it to be immediate and I can't find a solution.

Any help ?

Lemma mxdirect_delta (F : fieldType) (T : finType)
  (n : nat) (P : pred T) (f : T -> 'I_n) :
  injective f ->
  mxdirect (\sum_(i | P i) <<delta_mx 0 (f i) : 'rV[F]_n>>)%MS.

Best,
-- 
Cyril