English
The exponential of a block-diagonal matrix with blocks v(i) is the block-diagonal of the exponentials of the blocks: exp(blockDiagonal v) = blockDiagonal (exp v).
Русский
Экспонента блочно-диагональной матрицы, состоящей из блоков v(i), равна блочно-диагонали экспонент блоков: exp(blockDiagonal v) = blockDiagonal (exp v).
LaTeX
$$$\\exp\\_\\mathbb{K}(\\operatorname{blockDiagonal} v) = \\operatorname{blockDiagonal}(\\exp\\_\\mathbb{K} v)$$$
Lean4
theorem exp_blockDiagonal (v : m → Matrix n n 𝔸) : exp 𝕂 (blockDiagonal v) = blockDiagonal (exp 𝕂 v) := by
simp_rw [exp_eq_tsum, ← blockDiagonal_pow, ← blockDiagonal_smul, ← blockDiagonal_tsum]