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