English
Powers of a block-diagonal matrix with diagonal blocks A and D are computed blockwise: (fromBlocks A 0 0 D)^k = fromBlocks (A^k) 0 0 (D^k).
Русский
Степени блочно-диагональной матрицы с диагональными блоками A и D вычисляются по блокам: (fromBlocks A 0 0 D)^k = fromBlocks (A^k) 0 0 (D^k).
LaTeX
$$$ (\\text{fromBlocks } A \\ 0 \\ 0 \\ D)^k = \\text{fromBlocks }(A^k) 0 0 (D^k) $$$
Lean4
theorem fromBlocks_multiply [Fintype l] [Fintype m] [NonUnitalNonAssocSemiring α] (A : Matrix n l α) (B : Matrix n m α)
(C : Matrix o l α) (D : Matrix o m α) (A' : Matrix l p α) (B' : Matrix l q α) (C' : Matrix m p α)
(D' : Matrix m q α) :
fromBlocks A B C D * fromBlocks A' B' C' D' =
fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') :=
by
ext i j
rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;>
simp only [fromBlocks, mul_apply, of_apply, Sum.elim_inr, Fintype.sum_sum_type, Sum.elim_inl, add_apply]
