Zulip Chat Archive

Stream: general

Topic: matrices


view this post on Zulip Andrew Ashworth (Apr 07 2018 at 22:50):

any of the coq experts out there know what the most complete linalg / tensor package is out there for theorem provers? I'd like to look into what's out there for computing with complex matrices. quaternions would be cool too

view this post on Zulip Andrew Ashworth (Apr 07 2018 at 22:58):

the top referenced paper is this: http://www.math.ias.edu/~amortberg/papers/coqeal.pdf

view this post on Zulip Yulia Zaplatina (Jul 13 2018 at 10:40):

I am slightly stuck on the definition of a GL group, has anyone defined matrices yet?

view this post on Zulip Kenny Lau (Jul 13 2018 at 10:40):

@Kevin Buzzard your year 2 student?

view this post on Zulip Kevin Buzzard (Jul 13 2018 at 10:45):

@Ellen Arlt wrote some very basic code for matrices -- defining not much more than addition and multiplication, but it might be enough to define GL. @Blair Shi @Blair Shi I should tell you about this too. I think that both of you might be thinking about linear algebra and more specifically finite-dimensional vector spaces.

Oh -- I found Ellen's code! https://github.com/kbuzzard/xena/blob/master/student_contributions/Ellen_Arlt_matrix_rings.lean . She proves that square matrices form a ring. @Kenny Lau presumably there is "units of a ring" somewhere?

view this post on Zulip Kenny Lau (Jul 13 2018 at 10:50):

yes

view this post on Zulip Kenny Lau (Jul 13 2018 at 10:50):

units \a

view this post on Zulip Kenny Lau (Jul 13 2018 at 10:50):

works for fake rings also

view this post on Zulip Yulia Zaplatina (Jul 13 2018 at 10:50):

@Kevin Buzzard Thank you!

view this post on Zulip Yulia Zaplatina (Jul 13 2018 at 10:53):

Could we add @Ellen Arlt 's code to mathlib so we don't have to define matrices every time?

view this post on Zulip Blair Shi (Jul 13 2018 at 11:11):

Wow, I think this might be useful for my vector space. Thank you for telling me about this.

view this post on Zulip Kevin Buzzard (Jul 13 2018 at 12:37):

I think it would be easier to just put it into our UROP repo. It's time to start a xenalib!

view this post on Zulip Simon Hudon (Jul 13 2018 at 13:54):

@Kevin Buzzard @Ellen Arlt I suggest you remove the ring constraint in:

definition matrix (R: Type) (n m : nat)[ring R] :=  fin n ( fin m  R )

It makes it less useable in new and creative ways and it doesn't add any value: the ring assumption is really useful only for the operations and lemmas.

view this post on Zulip Kevin Buzzard (Jul 13 2018 at 14:32):

I'm busy today doing admin but I dumped ellen's code and Sean's comments on it here https://github.com/ImperialCollegeLondon/xena-UROP-2018/tree/master/src/xenalib

view this post on Zulip Kevin Buzzard (Jul 13 2018 at 14:34):

@Yulia Zaplatina if you pull the xena-UROP-2018 repo and open the folder in VS Code then you should be able to type stuff like import xenalib/Ellen_Arlt_matrix_rings and get her definitions. Someone should merge Sean's edits as well but I need to go and throw eggs at Trump


Last updated: May 08 2021 at 10:12 UTC