Ssreflect Users Discussion List

[Laurent Théry <>]

On 05/13/2011 11:34 AM, bertot wrote:
> Hello,
>
> As a tutorial example for working in the Formath european project, I 
> have been trying to describe functions on matrices, where the matrices 
> are represented by lists of lines, and prove the correctness of these 
> functions using ssreflect and the mathematical knowledge in 
> math-components.
>
> Unfortunately, I move much slower than I wanted and I will be happy to 
> have comments from other users.  In particular, I a just now blocked 
> by two questions:
>
> - What is the determinant of a 0x0 matrix (it should be 1, but I have 
> a hard time to prove it).  In particular, can I show that big sum in 
> the definition of determinant will only iterate over a one element 
> list (the identity permutation is the only permutation in 'S_0).
Lemma det0 : forall (R : comRingType) (M: 'M[R]_0) ,  \det M = 1.
Proof. by move=> R M; rewrite -[1](det1 R 0) [M]flatmx0 [1%:M]flatmx0. Qed.

--
Laurent