# 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: May 08 2021 at 10:12 UTC