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]