charmatrix_toSquareBlock — Mathlib

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]

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