lieEquivMatrix'_symm_apply — Mathlib

English

The inverse of the Lie equivalence maps a matrix A to the corresponding linear map: (lieEquivMatrix')^{-1} A = Matrix.toLin' A.

Русский

Обратное отображение тождественного перехода переводит матрицу A обратно в линейное отображение: (lieEquivMatrix')^{-1} A = Matrix.toLin' A.

LaTeX

$$$(\\mathrm{lieEquivMatrix'})^{-1} A = \\mathrm{Matrix.toLin'}(A).$$$

Lean4

@[simp]
theorem lieEquivMatrix'_symm_apply (A : Matrix n n R) : (@lieEquivMatrix' R _ n _ _).symm A = Matrix.toLin' A :=
  rfl

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