Theorems · Inductive type · nonassociative algebras

IsSl2Triple.HasPrimitiveVectorWith

{R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [Module R M] → [LieRingModule L M] → {h e f : L} → IsSl2Triple h e f → M → R → Prop

Given a representation of a Lie algebra with distinguished sl₂ triple, a vector is said to be primitive if it is a simultaneous eigenvector for the action of both h and e, and the eigenvalue for e is zero.

Defined in

Mathlib.Algebra.Lie.Sl2

Cited by

15 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CommRingLieRingAddCommGroupModuleLieRingModule