English
There is a Frobenius-based normed ring structure on the square matrices M_m(α); the Frobenius norm induces the ring operations compatibly.
Русский
Для квадратных матриц M_m(α) существует структурa нормированной кольцевой области, нормa Фробениуса совместима с умножением и сложением.
LaTeX
$$Normed ring structure on M_m(α) with Frobenius norm$$
Lean4
/-- Normed ring instance (using the Frobenius norm) for matrices over `ℝ` or `ℂ`. Not
declared as an instance because there are several natural choices for defining the norm of a
matrix. -/
@[local instance]
def frobeniusNormedRing [DecidableEq m] : NormedRing (Matrix m m α) :=
{ Matrix.frobeniusSeminormedAddCommGroup,
Matrix.instRing with
norm := Norm.norm
norm_mul_le := frobenius_norm_mul
eq_of_dist_eq_zero := eq_of_dist_eq_zero }
