fromBlocks_one — Mathlib

English

Let l and m be index sets. The block matrix formed by placing identity blocks on the diagonal equals the identity on the combined index set.

Русский

Пусть существуют индексы l и m. Блочная матрица, состоящая из единичных блоков на диагонали, равна единичной матрице на объединённом индексе.

LaTeX

$$$\operatorname{fromBlocks}\bigl(I_l, 0, 0, I_m\bigr) = I_{l \oplus m}.$$$

Lean4

@[simp]
theorem fromBlocks_one : fromBlocks (1 : Matrix l l α) 0 0 (1 : Matrix m m α) = 1 :=
  by
  ext i j
  rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp [one_apply]

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