mathlib

e42cfdb0 - chore(linear_algebra/matrix/to_linear_equiv): golf using existing morphisms (#18895)

chore(linear_algebra/matrix/to_linear_equiv): golf using existing morphisms (#18895) Also changes the statement of `matrix.to_linear_equiv'_symm_apply` to be `rfl`, since it's easy to change to another spelling at the call site.