Ssreflect Users Discussion List

[Georges Gonthier <>]

barring the m=0 case, you could use the additive group structure on 'I_(m + 
n).
Here, or course, it's much easier to give M = block_mx 0 1%:M 1%:M 0...
   Georges

-----Original Message-----
From: Vincent Siles [] 
Sent: 05 April 2012 09:59
To: 
Subject: building a translation permutation

Hi everyone,

my final goal is to prove that
forall m n (I: 'rV[R]_m) (J: 'rV[R]_n), exists M, row_mx I J = (row_mx J I) 
*m M

I think the easiest way to prove this is to "translate" all columns of row_mx 
I J to the  right by n position, as in :  { 0 1 | 2 3 4} -> {2 3 4 | 0 1 } 
With this, I should get to row_mx J I, so I guess that M is a permutation 
matrix (with a nice cast around it). My problem is that I can manage to 
define this permutation.

Is there an easy way to define this translation permutation ?

Best,
Vincent