Theorems · Definition · nonassociative algebras

skewAdjointMatricesLieSubalgebraEquivTranspose

{R : Type u} →
  {n : Type w} →
    [inst : CommRing R] →
      [inst_1 : Fintype n] →
        (J : Matrix n n R) →
          [inst_2 : DecidableEq n] →
            {m : Type w} →
              [inst_3 : DecidableEq m] →
                [inst_4 : Fintype m] →
                  (e : Matrix n n R ≃ₐ[R] Matrix m m R) →
                    (∀ (A : Matrix n n R), (e A).transpose = e A.transpose) →
                      ↥(skewAdjointMatricesLieSubalgebra J) ≃ₗ⁅R⁆ ↥(skewAdjointMatricesLieSubalgebra (e J))

An equivalence of matrix algebras commuting with the transpose endomorphisms restricts to an equivalence of Lie algebras of skew-adjoint matrices.

Defined in

Mathlib.Algebra.Lie.SkewAdjoint

Cited by

1 results in Mathlib

Foundations

Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingFintypeDecidableEqDecidableEqFintype