Theorems · Definition · nonassociative algebras

LieAlgebra.Basis.equivOfReindex

{ι₁ : Type u_1} →
  {ι₂ : Type u_2} →
    {L₁ : Type u_3} →
      {L₂ : Type u_4} →
        [inst : Finite ι₁] →
          [inst_1 : Finite ι₂] →
            (eι : ι₁ ≃ ι₂) →
              [inst_2 : LieRing L₁] →
                [inst_3 : LieRing L₂] →
                  {K : Type u_5} →
                    [inst_4 : Field K] →
                      [CharZero K] →
                        [inst_6 : LieAlgebra K L₁] →
                          [FiniteDimensional K L₁] →
                            {H₁ : LieSubalgebra K L₁} →
                              (b₁ : LieAlgebra.Basis ι₁ H₁) →
                                [inst_8 : LieAlgebra K L₂] →
                                  [FiniteDimensional K L₂] →
                                    {H₂ : LieSubalgebra K L₂} →
                                      (b₂ : LieAlgebra.Basis ι₂ H₂) →
                                        (Matrix.reindex eι eι) b₁.A = b₂.A →
                                          [LieAlgebra.IsSimple K L₁] → [LieAlgebra.IsSimple K L₂] → L₁ ≃ₗ⁅K⁆ L₂

Simple Lie algebras with equivalent bases are equivalent.

Defined in

Mathlib.Algebra.Lie.Basis.Prod

Cited by

0 results in Mathlib

Foundations

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

Assumes

FiniteFiniteLieRingLieRingFieldCharZeroLieAlgebraFiniteDimensionalLieAlgebraFiniteDimensionalLieAlgebra.IsSimpleLieAlgebra.IsSimple