Topic: matrix updates
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.
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.
Johan Commelin (Sep 11 2018 at 09:32):
Cool, so now matrices are even a ring. Nice work Sean!
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.
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).
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!
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.
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