Stream: maths

Topic: matrix.congr

Johan Commelin (Dec 11 2020 at 14:08):

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 (Dec 11 2020 at 14:37):

That's just arrow_congr applied twice, right?

Kevin Buzzard (Dec 11 2020 at 14:46):

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

Oliver Nash (Dec 11 2020 at 14:46):

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 (Dec 11 2020 at 14:49):

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

Johan Commelin (Dec 11 2020 at 14:49):

@Oliver Nash thanks a lot

Last updated: May 14 2021 at 18:28 UTC