Johan Commelin (Feb 28 2019 at 08:50):
Another question about file organisation: why is
ring_theory/ instead of
Johannes Hölzl (Feb 28 2019 at 08:58):
I would even move
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):
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)
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
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 and , 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