English
For matrices over a seminormedAddCommGroup, one can define a Frobenius-type seminorm by summing the squares of the entry norms and taking the square root.
Русский
Для матриц над полем семиномормированного типа можно определить семиноморную норму Фробениуса как корень из суммы квадратов норм элементов, суммированной по всем позициям.
LaTeX
$$$\|A\| = \left( \sum_i \sum_j \|A_{ij}\|^2 \right)^{1/2}.$$$
Lean4
/-- Seminormed group instance (using the Frobenius norm) for matrices over a seminormed group. Not
declared as an instance because there are several natural choices for defining the norm of a
matrix. -/
@[local instance]
def frobeniusSeminormedAddCommGroup [SeminormedAddCommGroup α] : SeminormedAddCommGroup (Matrix m n α) :=
inferInstanceAs (SeminormedAddCommGroup (PiLp 2 fun _i : m => PiLp 2 fun _j : n => α))
