Zulip Chat Archive

Stream: maths

Topic: matrix.congr


view this post on Zulip 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?

view this post on Zulip Eric Wieser (Dec 11 2020 at 14:37):

That's just arrow_congr applied twice, right?

view this post on Zulip Oliver Nash (Dec 11 2020 at 14:44):

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

view this post on Zulip Kevin Buzzard (Dec 11 2020 at 14:46):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Dec 11 2020 at 14:49):

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

view this post on Zulip Johan Commelin (Dec 11 2020 at 14:49):

@Oliver Nash thanks a lot


Last updated: May 14 2021 at 18:28 UTC