isUnit_exp — Mathlib

English

Let A be a square matrix over a normed algebra. Then the matrix exponential exp(𝕂, A) is invertible, with inverse exp(𝕂, −A).

Русский

Пусть A — квадратная матрица над нормированной алгеброй. Тогда экспонента матрицы exp(A) является обратимой, обратная экспонента равна exp(−A).

LaTeX

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

Lean4

nonrec theorem isUnit_exp (A : Matrix m m 𝔸) : IsUnit (exp 𝕂 A) :=
  open scoped Norms.Operator in isUnit_exp _ A

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