Define matrices as a collection of columns rather than a collection of rows

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory

http://homotopytypetheory.org/

Other

1.23k stars 185 forks source link

Define matrices as a collection of columns rather than a collection of rows #1983

Open Alizter opened 1 month ago

Alizter commented 1 month ago

Currently we define matrices as a vector of rows. Given how matrix multiplication usually acts on the left on column vectors, it might be worth redefining matrices as vectors of columns allowing us to derive results about amtrix multiplication from the analogous results on column vectors.