frobeniusNormSMulClass — Mathlib

English

The Frobenius-normed matrix space carries a NormSMulClass structure over the base ring, i.e., scalar multiplication respects the norm in the usual way.

Русский

Пространство матриц с нормой Фробениуса имеет структуру NormSMulClass над основанием кольца, то есть умножение на скаляр сохраняет норму в обычном виде.

LaTeX

$$$\text{NormSMulClass } R (M_{m\times n}(\alpha)).$$$

Lean4

/-- This applies to the Frobenius norm. -/
@[local instance]
theorem frobeniusNormSMulClass [SeminormedRing R] [SeminormedAddCommGroup α] [Module R α] [NormSMulClass R α] :
    NormSMulClass R (Matrix m n α) :=
  (by infer_instance : NormSMulClass R (PiLp 2 fun i : m => PiLp 2 fun j : n => α))

Похожие утверждения