exp_diagonal — Mathlib

English

The exponential of a diagonal matrix equals the diagonal of the exponentials of the diagonal entries.

Русский

Экспонента диагональной матрицы равна диагонали экспонент соответствующих диагональных элементов.

LaTeX

$$$\\exp\\_\\mathbb{K} (\\operatorname{diag}(v)) = \\operatorname{diag}(\\exp\\_\\mathbb{K}(v))$$$

Lean4

theorem exp_diagonal (v : m → 𝔸) : exp 𝕂 (diagonal v) = diagonal (exp 𝕂 v) := by
  simp_rw [exp_eq_tsum, diagonal_pow, ← diagonal_smul, ← diagonal_tsum]

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