matrix

Stream: maths

[Johan Commelin]

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

[Johannes Hölzl]

I would even move matrix to data and determinant to linear_algebra

[Alexander Bentkamp]

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]

you can use a local notation for that

[Alexander Bentkamp]

ok

[Alexander Bentkamp]

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]

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

[Johan Commelin]

Whether that is a good reason is up for debate

[Johan Commelin]

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

[Johan Commelin]

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

[Alexander Bentkamp]

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