exp_neg

Mathlib.Analysis.Normed.Algebra.MatrixExponential

URI: https://scilib.ai/kg/mathlib#Matrix.exp_neg

← MathLib Explorer

English

For any square matrix A, exp(𝕂, −A) = (exp(𝕂, A))^{-1}.

Русский

Для любой квадратной матрицы A выполняется exp(−A) = (exp(A))^{-1}.

LaTeX

$$$\exp_{\mathbb{K}}(-A) = \big(\exp_{\mathbb{K}}(A)\big)^{-1}.$$$

Lean4

theorem exp_neg (A : Matrix m m 𝔸) : exp 𝕂 (-A) = (exp 𝕂 A)⁻¹ :=
  by
  rw [nonsing_inv_eq_ringInverse]
  open scoped Norms.Operator in exact (Ring.inverse_exp _ A).symm

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru