submatrix_smul — Mathlib

English

Scalar multiplication distributes over submatrix: ((r · A).submatrix) = r · A.submatrix.

Русский

Скалярное умножение распадается на подматрицу: ((r · A).submatrix) = r · A.submatrix.

LaTeX

$$$ (r \cdot A).submatrix = r \cdot A.submatrix $$$

Lean4

theorem submatrix_smul {R : Type*} [SMul R α] (r : R) (A : Matrix m n α) :
    ((r • A : Matrix m n α).submatrix : (l → m) → (o → n) → Matrix l o α) = r • A.submatrix :=
  rfl

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