Zulip Chat Archive

Stream: general

Topic: matrices

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

Andrew Ashworth (Apr 07 2018 at 22:58):

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

Yulia Zaplatina (Jul 13 2018 at 10:40):

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

Kenny Lau (Jul 13 2018 at 10:40):

@Kevin Buzzard your year 2 student?

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?

Kenny Lau (Jul 13 2018 at 10:50):

yes

Kenny Lau (Jul 13 2018 at 10:50):

units \a

Kenny Lau (Jul 13 2018 at 10:50):

works for fake rings also

Yulia Zaplatina (Jul 13 2018 at 10:50):

@Kevin Buzzard Thank you!

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?

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.

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!

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.

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

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: Dec 20 2023 at 11:08 UTC