Zulip Chat Archive

Stream: maths

Topic: matrix


Johan Commelin (Feb 28 2019 at 08:50):

Another question about file organisation: why is matrix and determinant in ring_theory/ instead of linear_algebra/?

Johannes Hölzl (Feb 28 2019 at 08:58):

I would even move matrix to data and determinant to linear_algebra

Alexander Bentkamp (Apr 01 2019 at 19:06):

I'd like to improve the matrix library a bit. Is there a reason why there is no infix notation for matrix multiplication? Writing M.mul is not very pretty. How about M ⬝ N? I would also like to introduce for transpose.

Mario Carneiro (Apr 01 2019 at 19:07):

you can use a local notation for that

Alexander Bentkamp (Apr 01 2019 at 19:09):

ok

Alexander Bentkamp (Apr 03 2019 at 19:08):

Is there a reason why the order of arguments of matrix is:

matrix (m n : Type u) [fintype m] [fintype n] (α : Type v)

and not

matrix (α : Type v) (m n : Type u) [fintype m] [fintype n]

?
I think the latter makes much more sense.
Would anyone object if I refactor this?

Johan Commelin (Apr 03 2019 at 19:16):

The reason is that matrix m n is functorial in \alpha.

Johan Commelin (Apr 03 2019 at 19:17):

Whether that is a good reason is up for debate

Johan Commelin (Apr 03 2019 at 19:18):

In fact we haven't yet defined matrix.map I think.

Johan Commelin (Apr 03 2019 at 19:19):

But from a perspective of algebra it is natural to have the \alpha come last. Compare with the notation Mm,n(R)M_{m,n}(\mathbb{R}) and GLn(C)\mathrm{GL}_n(\mathbb{C}), etc...

Alexander Bentkamp (Apr 03 2019 at 19:22):

Ok, I see. Then I'll better leave it as is.


Last updated: Dec 20 2023 at 11:08 UTC