submatrix_add — Mathlib

English

The submatrix operator distributes over addition: ((A + B).submatrix) = A.submatrix + B.submatrix.

Русский

Оператор подматрицы распределяется по сложению: ((A + B).submatrix) = A.submatrix + B.submatrix.

LaTeX

$$$ ((A + B).submatrix) = A.submatrix + B.submatrix $$$

Lean4

theorem submatrix_add [Add α] (A B : Matrix m n α) :
    ((A + B).submatrix : (l → m) → (o → n) → Matrix l o α) = A.submatrix + B.submatrix :=
  rfl

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