Theorems · Definition · nonassociative algebras

skewAdjointMatricesLieSubalgebraEquiv

{R : Type u} →
  {n : Type w} →
    [inst : CommRing R] →
      [inst_1 : Fintype n] →
        (J : Matrix n n R) →
          [inst_2 : DecidableEq n] →
            (P : Matrix n n R) →
              Invertible P →
                ↥(skewAdjointMatricesLieSubalgebra J) ≃ₗ⁅R⁆ ↥(skewAdjointMatricesLieSubalgebra (P.transpose * J * P))

An invertible matrix P gives a Lie algebra equivalence between those endomorphisms that are skew-adjoint with respect to a square matrix J and those with respect to PᵀJP.

Defined in

Mathlib.Algebra.Lie.SkewAdjoint

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingFintypeDecidableEq