hhu-adam / Robo

A game for learning lean 4 where a cute little Robo joins you on your exploration of the Mathiverse. The game is in German 🇩🇪
https://adam.math.hhu.de
Apache License 2.0
16 stars 9 forks source link

MatrixTrace: Can we typeset some matrices in earlier levels to improve readability? #48

Closed TentativeConvert closed 2 months ago

TentativeConvert commented 2 months ago

For example, level 1 asks us to show something A i j • E i j. The notation is confusing insofar as A i j is a scalar and E i j is a matrix. It might help to make use of latex to spell out in the chat that

A = \begin{matrix} … A i j … \end{matrix} 

and

E i j = \begin{matrix} … \end{matrix}

to clarify how this is to be read.

TentativeConvert commented 2 months ago

Done: bed81540be524ee91e5b34950543faaa4609ba7d