Ssreflect Users Discussion List

[Georges Gonthier <>]

  I usually use the mx11_scalar lemma to deal with 1x1 matrices; in the 
reverse direction it can be used to change the rhs to
col_mx (usubmx C) 0, then that last 0 can be changed to dsubmx (C : 'M_(1 + 
0)) with flatmx0, and with vsubmxK and mul1mx you'll be done.
 However, somehow you shouldn't be getting an equation between matrices with 
different shapes, so there ought to be something wrong with the way you set 
up your proof.

   Georges

-----Original Message-----
From: Vincent Siles [] 
Sent: 19 May 2011 16:35
To: 
Subject: basic question about matrices

Hi everyone,
I'm trying to learn how to use the matrix library of ssreflect, and I'm a bit 
lost.
On one of my easy case, I have a 1x1 matrix, and I want to prove the 
following property

  C : 'M_1
  ============================
   1%:M *m C = col_mx ((usubmx C) ord0 ord0)%:M 0

Is there a way to tell ssreflect "C is a 1x1 matrix, so just extract its 
value from the matrix" ?

How can I get read of the col_mx ? (if I'm right, the left part is a
1x1 matrix, so the col_mx ... 0
should disappear ?)


Cheers,
Vincent