Theorems · Definition · nonassociative algebras

LieAlgebra.Basis.baseSupportEquiv

{ι : Type u_1} →
  {K : Type u_2} →
    {L : Type u_3} →
      [inst : Fintype ι] →
        [inst_1 : Field K] →
          [inst_2 : CharZero K] →
            [inst_3 : LieRing L] →
              [inst_4 : LieAlgebra K L] →
                [inst_5 : FiniteDimensional K L] →
                  {H : LieSubalgebra K L} →
                    (b : LieAlgebra.Basis ι H) →
                      [inst_6 : LieModule.IsTriangularizable K (↥H) L] →
                        [inst_7 : LieAlgebra.IsKilling K L] → ι ≃ ↥b.base.support

The support of LieAlgebra.Basis.base is in one-to-one correspondence with the indexing set of the basis.

Defined in

Mathlib.Algebra.Lie.Basis.Base

Cited by

3 results in Mathlib

Foundations

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

Assumes

FintypeFieldCharZeroLieRingLieAlgebraFiniteDimensionalLieModule.IsTriangularizableLieAlgebra.IsKilling