The Coq mailing list

[Jasper Stein <jasper AT cs.kun.nl>]

Dear coq users,

I am happy to announce a new contribution: linear algebra.

The linear algebra contribution formalises the basics of (general) 
linear algebra and is based on the first chapter of Friedberg, Insel and 
Spence's book "Linear Algebra", 2nd edition, (c)1989, 1979 by 
Prentice-Hall, Inc., ISBN 0-13-536855-3.

This contribution extends Loic Pottier's "algebra" contribution.

"linear algebra" will be available from the contributions page of the 
Coq website as soon as it is updated. Meanwhile it can be downloaded 
from http://www.cs.kun.nl/~jasper/WWW/LinAlg.tar.gz

- Vectorspaces
- Subspaces
- Linear combinations
- Linear (in)dependence
- Spans
- Bases
- Dimensions
- Many supportive definitions and lemmas
- (A few) examples
- PostScript documentation (needs coqdoc)
- Install script

Jasper
--
Het verschil tussen theorie en praktijk is dat in theorie
er geen verschil is tussen theorie en praktijk.