Ssreflect Users Discussion List

[Nicolas Magaud <>]

Dear all,

I recently started using ssreflect to describe bits and pieces of discrete 
geometry.
Some operations I use are represented as matrices and I need to define a 
function which given a vector $V$, computes $A*V+B$ when $A$ is a square 
matrix (2x2 or 3x3) and $B$ another vector.
My matrices are non-empty (n<>0), but the carrier is not a field. However it 
seems not to be an issue (from what I read in matrix.v).

I tried and used the notations +m and *m without success. While making 
experiments, I also faced some issues with \trace and \det which I do not 
manage to use properly.

The code I have so far looks like the (simplified) one attached (o.v). I 
guess this might look like simple questions to most of you. Howerver some 
assistance in getting started would be appreciated.

Best regards,

Nicolas Magaud

Attachment: o.v
Description: Binary data