## 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

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 $M_{m,n}(\mathbb{R})$ and $\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: May 19 2021 at 02:10 UTC