exp_blockDiagonal — Mathlib

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]

Похожие утверждения