submatrix_one_embedding — Mathlib

English

For embedding e, the submatrix of the identity by e is the identity of the smaller index set.

Русский

Для вложения e подматрица единицы по e равна единице меньшего размера.

LaTeX

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

Lean4

@[simp]
theorem submatrix_one_embedding [Zero α] [One α] [DecidableEq m] [DecidableEq l] (e : l ↪ m) :
    (1 : Matrix m m α).submatrix e e = 1 :=
  submatrix_one e e.injective

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