Zulip Chat Archive

Stream: maths

Topic: matrix updates


view this post on Zulip Sean Leather (Sep 11 2018 at 08:21):

@Kevin Buzzard I worked a bit on matrices on the side. I don't know if you'll be happy with the differences with #334, so I PR'd #2 to your branch on leanprover-community/mathlib. Let me know what you think.

view this post on Zulip Sean Leather (Sep 11 2018 at 08:24):

BTW, to view the diff while ignoring whitespace changes, see https://github.com/leanprover-community/mathlib/pull/2/files?w=1 . There are still a lot of changes. :concerned: But I believe all of the major stuff that was in your original PR is still there.

view this post on Zulip Johan Commelin (Sep 11 2018 at 09:32):

Cool, so now matrices are even a ring. Nice work Sean!

view this post on Zulip Johan Commelin (Sep 11 2018 at 09:33):

I agree that the diff looks a bit daunting. But I think that is mostly because of some syntactic changes that don't represent a very big change in mathematics.

view this post on Zulip Kevin Buzzard (Sep 11 2018 at 10:03):

I am completely happy with any changes. I am just tired of matrices not being in Lean (as are some of my "clients", as Mario once referred to them).

view this post on Zulip Kevin Buzzard (Sep 11 2018 at 10:32):

PS @Johan Commelin Ellen proved they were a ring :P . @Sean Leather I should also add -- thanks a lot!

view this post on Zulip Sean Leather (Sep 11 2018 at 10:41):

Yes, all the credit should go to people who worked on it before me. I just build on the shoulders of giants. Also, I think the fintype idea was due to Johannes and Johan. Since Kevin is happy, I merged the PR.

view this post on Zulip Johan Commelin (Sep 12 2018 at 04:57):

Somehow Travis is now failing (and it is not a timeout). It didn't receive any output for 10min.


Last updated: May 18 2021 at 06:15 UTC