lieConj — Mathlib

English

An invertible matrix P induces a Lie algebra automorphism on matrices by conjugation: A ↦ P A P^{-1}.

Русский

Обратимая матрица P индуцирует по отношению к матрицам автоморфизм Ли: A ↦ P A P^{-1}.

LaTeX

$$$P.lieConj h(A) = P A P^{-1}$ for invertible P and A a matrix.$$

Lean4

/-- An invertible matrix induces a Lie algebra equivalence from the space of matrices to itself. -/
def lieConj (P : Matrix n n R) (h : Invertible P) : Matrix n n R ≃ₗ⁅R⁆ Matrix n n R :=
  ((@lieEquivMatrix' R _ n _ _).symm.trans (P.toLinearEquiv' h).lieConj).trans lieEquivMatrix'

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