English
There is a canonical display format for finite matrices: a matrix A ∈ M_{m×n}(α) is shown as a 2D array with rows separated by semicolons, inside a special bracket structure, provided α has a representation.
Русский
Существует канонический формат отображения конечной матрицы: матрица A ∈ M_{m×n}(α) выводится как двумерный массив с разделением строк точками с запятой внутри специальной скобочной конструкции, если α имеет представление.
LaTeX
$$$\\text{repr}(A) = !!\\left[\\text{row}_1; \\cdots ; \\text{row}_m\\right], \\quad \\text{где строки задаются элементами } A$$$
Lean4
/-- Use `![...]` notation for displaying a `Fin`-indexed matrix, for example:
```
#eval !![1, 2; 3, 4] + !![3, 4; 5, 6] -- !![4, 6; 8, 10]
```
-/
instance repr [Repr α] : Repr (Matrix (Fin m) (Fin n) α) where
reprPrec f
_p :=
(Std.Format.bracket "!![" · "]") <|
(Std.Format.joinSep · (";" ++ Std.Format.line)) <|
(List.finRange m).map fun i =>
Std.Format.fill <| -- wrap line in a single place rather than all at once
(Std.Format.joinSep · ("," ++ Std.Format.line)) <| (List.finRange n).map fun j => _root_.repr (f i j)
