map_toSquareBlock — Mathlib

English

Let f: α → β and M be a square matrix with entries in α. Then applying f entrywise commutes with extracting a square block: (M.map f).toSquareBlock b i = (M.toSquareBlock b i).map f.

Русский

Пусть f: α → β и M — квадратная матрица с элементами α. Применение f по элементам и извлечение квадратного блока коммутируют: (M.map f).toSquareBlock b i = (M.toSquareBlock b i).map f.

LaTeX

$$$(M.map\\ f)^{\\text{toSquareBlock}}_{b,i} = (M^{\\text{toSquareBlock}}_{b,i})\\cdot f$$$

Lean4

theorem map_toSquareBlock (f : α → β) {M : Matrix m m α} {ι} {b : m → ι} {i : ι} :
    (M.map f).toSquareBlock b i = (M.toSquareBlock b i).map f :=
  submatrix_map _ _ _ _

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