English
A block matrix with diagonal blocks from diagonal operators equals a diagonal matrix whose diagonal entries are the concatenation (Sum.elim) of the two diagonal sequences.
Русский
Блочная матрица с диагональными блоками из диагоналей равна диагональной матрице, чьи диагональные элементы получены объединением Sum.elim двух последовательностей.
LaTeX
$$$ \\text{fromBlocks }(\\text{diagonal } d_1) \\ 0 \\ 0 \\ (\\text{diagonal } d_2) = \\text{diagonal } (\\text{Sum.elim } d_1 d_2) $$$
Lean4
theorem fromBlocks_diagonal_pow [Semiring α] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (A : Matrix n n α)
(D : Matrix m m α) (k : ℕ) : (fromBlocks A 0 0 D) ^ k = fromBlocks (A ^ k) 0 0 (D ^ k) := by
induction k with
| zero => ext (i | i) (j | j) <;> simp [one_apply]
| succ n ih => simp [ih, pow_succ, fromBlocks_multiply]
