The Linear Algebra distribution by Jasper Stein ([email protected]) extending the (required) algebra distribution by Loic Pottier, and following Chapter 1 of "Linear Algebra" by Friedberg, Insel and Spence.
Available as package coq-lin-alg via OPAM.
Share and enjoy! Jasper Stein