exp_blockDiagonal' — Mathlib

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]

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