# formalization of coordinate-free linear algebra in a proof assistant

I am aware of projects that formalize linear algebra in existing proof assistants (i.e. Coq), but it seems like most of them are based on matrices. I was wondering if it's done in a coordinate-free way, with operations like taking tensor/wedge powers and dualizing. If so, at least in the finite dimensional case, can one coordinatize and work with matrices?