submatrix_one — Mathlib

English

If e: l → m is injective, then the submatrix of the identity matrix along e is the identity matrix of the smaller size.

Русский

Если e: l → m инъективно, то подматрица единичной матрицы по индексам e равна единичной матрице меньшего размера.

LaTeX

$$$\bigl(1_{m\times m}\bigr)_{e,e} = 1_{l\times l}$$$

Lean4

theorem submatrix_one [Zero α] [One α] [DecidableEq m] [DecidableEq l] (e : l → m) (he : Function.Injective e) :
    (1 : Matrix m m α).submatrix e e = 1 :=
  submatrix_diagonal _ e he

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