mathlib3

ccd35db8 - feat(linear_algebra/matrix): to_matrix and to_lin as alg_equiv (#6496)

feat(linear_algebra/matrix): to_matrix and to_lin as alg_equiv (#6496) The existing `linear_map.to_matrix` and `matrix.to_lin` can be upgraded to an `alg_equiv` if working on linear endomorphisms or square matrices. The API is copied over in rote fashion. Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>