skewAdjointMatricesLieSubalgebraEquivTranspose_apply

English

An equivalence of matrix algebras that commutes with transpose endomorphisms restricts to a Lie algebra equivalence between skew-adjoint Lie subalgebras.

Русский

Эквивалентность матричных алгебр, которая коррелирует с транспонированием, ограничивает Ли-эквивалентность между косо‑сопряжёнными подалгебрами.

LaTeX

$$Restriction of e to skewAdjointMatricesLieSubalgebra J gives a LieEquiv to skewAdjointMatricesLieSubalgebra (e J) when eᵀ = eᵀ.$$

Lean4

@[simp]
theorem skewAdjointMatricesLieSubalgebraEquivTranspose_apply {m : Type w} [DecidableEq m] [Fintype m]
    (e : Matrix n n R ≃ₐ[R] Matrix m m R) (h : ∀ A, (e A)ᵀ = e Aᵀ) (A : skewAdjointMatricesLieSubalgebra J) :
    (skewAdjointMatricesLieSubalgebraEquivTranspose J e h A : Matrix m m R) = e A :=
  rfl

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