The Matrix Cookbook (November 15, 2012) [petersen2008matrix] covers many useful results about matrices, and Eric Wieser's project lean-matrix-cookbook aims to give one-liner proofs (with reference to the counter part in Mathlib) to all of them.
The project is far from complete and it would be great to claim a small portion of interested results and contribute to it. I also wish to figure out the GA counterpart of the same portion.
Previous interests about matrices rise from Steven De Keninck's work on GALM [de2019geometric], since the paper I have been interested in GA approaches that has practical advantages over traditional matrix-based methods. Notably the paper also discussed the link between degenerate Clifford algebras and dual numbers / automatic differentiation. A more recent inspiration might be his new work LookMaNoMatrices.
TODO: decide which results are interesting and feasible to be formalized for me.
I wish to pursue further on the topic of Matrix/Tensor, see [taylor2024introduction] and [randy2023matrix]. The former also led me to Einsums in C++. For the latter, I'm thinking of HepLean.SpaceTime.CliffordAlgebra.