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 _ _ _ _