English
The charmatrix of a matrix's toSquareBlock equals the toSquareBlock of the charmatrix: (M.toSquareBlock b a).charmatrix = M.charmatrix.toSquareBlock b a.
Русский
Характеристическая матрица блока toSquareBlock матрицы совпадает с блоком charmatrix самой матрицы: (M.toSquareBlock b a).charmatrix = M.charmatrix.toSquareBlock b a.
LaTeX
$$$\,(M.toSquareBlock\, b\, a).charmatrix = M.charmatrix.toSquareBlock b a$$$
Lean4
theorem charmatrix_toSquareBlock {α : Type*} [DecidableEq α] {b : n → α} {a : α} :
(M.toSquareBlock b a).charmatrix = M.charmatrix.toSquareBlock b a :=
by
ext i j : 1
simp [charmatrix_apply, toSquareBlock_def, diagonal_apply, Subtype.ext_iff]