submatrix_one_equiv — Mathlib

English

For an equivalence e: l ≃ m, the submatrix of the identity via e is the identity of the target size.

Русский

Для эквивалентности e: l ≃ m подматрица единицы вдоль e равна единице соответствующего размера.

LaTeX

$$$(\mathbf{1}_{m\times m})_{\text{coe } e, \text{coe } e} = \mathbf{1}_{l\times l}$$$

Lean4

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

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