English
Let R be a seminormed ring and α a seminormed additive commutative group equipped with an R-module structure, with IsBoundedSMul R α. Then the matrix space M_{m×n}(α) inherits a bounded R-action, i.e., ∥r · A∥ ≤ ∥r∥ ∥A∥ for all r ∈ R, A ∈ M_{m×n}(α).
Русский
Пусть R — полупорядоченное кольцо с нормой, α — семинормированная аддитивная коммутативная группа с R-модулем, и IsBoundedSMul R α. Тогда пространство матриц M_{m×n}(α) наследует ограниченное действие скаляра R: ∥r · A∥ ≤ ∥r∥ ∥A∥ для всех r∈R, A∈M_{m×n}(α).
LaTeX
$$$\\|r \\cdot A\\| \\leq \\|r\\| \\cdot \\|A\\| \\quad(\\forall r \\in R, A \\in \\mathrm{Mat}_{m\\times n}(\\alpha))$$$
Lean4
/-- This applies to the sup norm of sup norm. -/
protected theorem isBoundedSMul [SeminormedRing R] [SeminormedAddCommGroup α] [Module R α] [IsBoundedSMul R α] :
IsBoundedSMul R (Matrix m n α) :=
Pi.instIsBoundedSMul
