skewAdjointMatricesLieSubalgebraEquiv_apply

English

The action of the equivalence on a skew-adjoint matrix A yields its image under conjugation by P.

Русский

Действие эквивалентности на кососопряжённую матрицу A даёт её образ при конъюгации P.

LaTeX

$$(skewAdjointMatricesLieSubalgebraEquiv J P h A) = P^{-1} A P$$

Lean4

theorem skewAdjointMatricesLieSubalgebraEquiv_apply (P : Matrix n n R) (h : Invertible P)
    (A : skewAdjointMatricesLieSubalgebra J) : ↑(skewAdjointMatricesLieSubalgebraEquiv J P h A) = P⁻¹ * A * P := by
  simp [skewAdjointMatricesLieSubalgebraEquiv]

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