Theorems · Definition · nonassociative algebras

IsSl2Triple.HasPrimitiveVectorWith.recOn

{R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] →
              [inst_4 : LieRingModule L M] →
                {h e f : L} →
                  {t : IsSl2Triple h e f} →
                    {m : M} →
                      {μ : R} →
                        {motive : t.HasPrimitiveVectorWith m μ → Sort u} →
                          (t_1 : t.HasPrimitiveVectorWith m μ) →
                            ((ne_zero : m ≠ 0) → (lie_h : ⁅h, m⁆ = μ • m) → (lie_e : ⁅e, m⁆ = 0) → motive ⋯) →
                              motive t_1

Defined in

Mathlib.Algebra.Lie.Sl2

Cited by

0 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext

Assumes

CommRingLieRingAddCommGroupModuleLieRingModule