Ssreflect Users Discussion List

[Xavier Allamigeon <>]

Dear MathComp-list,

I was wondering whether there is a way to manipulate matrices over a 
subring and mix them with matrices over the original ring.

More precisely, suppose that R has type ringType, and that R' is a 
subtype of R equipped with a structure of subring (provided by 
SubRingPred). Then, M[R']_(m,n) should be a subgroup of M[R]_(m,n), but 
I don't see any construction in MathComp to get this structure.
For instance, if A, B : M[R']_(m,n), and C : M[R]_(n,p), then I would 
like to recover that
A *m C + B *m C = (A + B) *m C
where the addition on the RHS is then one over M[R']_(m,n).
I cannot even find any default coercion from M[R']_(m,n) to M[R]_(m,n). 
Should it be defined by hand?

In my case, R' turns out to be a field, and I really need to exploit 
this special structure since then I'll be able to use the properties 
defined in mxalgebra.

Any hint?

Thanks in advance,
Xavier