linear_map.to_matrix_alg_equiv

Stream: maths

[Chris Hughes]

We currently have two versions of linear_map.to_matrix, one is a linear_equiv, and we also have linear_map.to_matrix_alg_equiv which is an algebra equivalence. Do we need both versions. The reason this came to my attention is because my PR #9249 didn't build because the following failed to simplify ⇑(to_matrix b b) (⇑(algebra_map R (module.End R S)) x) i i = x. If to_matrix was an alg_equiv then I think simp would have solved the goal.

[Yakov Pechersky]

docs#linear_map.to_matrix, docs#linear_map.to_matrix_alg_equiv

[Yakov Pechersky]

The former works on rectangular matrices. You can't have an alg equiv of nonsquare matrices, iirc