matrix.congr

Stream: maths

[Johan Commelin]

If we have equivalences of fintypes k =~ m and l =~ n, do we have the ring isom matrix k l R =~ matrix m n R?

[Eric Wieser]

That's just arrow_congr applied twice, right?

[Oliver Nash]

I think you might want https://leanprover-community.github.io/mathlib_docs/linear_algebra/matrix.html#matrix.reindex_alg_equiv

[Kevin Buzzard]

Aah, Johan's question makes no sense :-)

[Oliver Nash]

That :point_up: is for square matrices but if k ≠ l then matrix k l R isn't a ring. In this case, we have https://leanprover-community.github.io/mathlib_docs/linear_algebra/matrix.html#matrix.reindex_linear_equiv

[Johan Commelin]

ooh, good point. I meant equiv of modules (-;

[Johan Commelin]

@Oliver Nash thanks a lot