Hi,

I'm a close-to-beginner formalizing some (basic) combinatorial results for fun and to get a better hold on coq. I want to use linear-algebraic methods for some of this (in particular, Berlekamp's oddtown theorem). So far I've been using mathcomp's matrix.v, but it doesn't *seem* to have some basic-ish results I need. In particular:

1) (under some algebraic conditions on the base ring) The determinant of `A`

is 0 <-> there is a nontrivial linear relation among the cols, equivalently rows

2) (under some conditions) The matrix A has full row-rank (row-full A) <-> there is not a nontrivial linear relation among the rows; in particular, if `v^T A = 0`

, then `v = 0`

(this is the 'right' way to state it, I think)

It's entirely possible that both of these and more are present in mathcomp in a form I didn't recognize. There is one direction of (2) (row_full_inj in matrix.v) giving that `v => A . v`

is injective if `A`

has full row rank, but I couldn't find the other.

I only really need these results for integer matrices, and eventually for matrices over a finite field (really just F_2, actually), and I don't know enough algebra to say what rings they hold on in general, so I wonder if I need to somehow specialize from mathcomp's framework of working over a generic ring to my specific domain.

Am I missing results mathcomp already has? Is there another library that has more robust linear algebra of this sort?

Or does it sound feasible to build up these results myself with what mathcomp has? I.e., define linear independence and use mathcomp's results to springboard to this type of thing. I don't have a sense of the feasibility of that sort of thing.

Thanks for any help!

Did you look at CoqEAL? It has various matrix-related results for MathComp: https://github.com/coq-community/coqeal

This topic was moved here from #Coq users > Linear Algebra Basics by Karl Palmskog.

(I think this fits better here due to the many MathComp references)

I will look into CoqEAL, thank you! Also, I just found (1) in matrix.v (det0P), so that's half of it solved as well.

this may be of interest w.r.t. linear algebra: https://github.com/VeriNum/LAProof

Last updated: Jul 25 2024 at 15:02 UTC