English
A variant of the block-diagonal exponential identity for a family v indexed by i: 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 : ∀ i, Matrix (n' i) (n' i) 𝔸) : exp 𝕂 (blockDiagonal' v) = blockDiagonal' (exp 𝕂 v) := by
simp_rw [exp_eq_tsum, ← blockDiagonal'_pow, ← blockDiagonal'_smul, ← blockDiagonal'_tsum]