Theorems · Theorem · nonassociative algebras

IsSl2Triple.mem_toLieSubalgebra_iff

∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {h e f x : L}
  {t : IsSl2Triple h e f}, x ∈ IsSl2Triple.toLieSubalgebra R t ↔ ∃ c₁ c₂ c₃, x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆

Defined in

Mathlib.Algebra.Lie.Sl2

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingLieRingLieAlgebra