Mathlib Map

Theorems · Theorem · nonassociative algebras

IsSl2Triple.lie_h_e_nsmul

∀ {L : Type u_2} [inst : LieRing L] {h e f : L}, IsSl2Triple h e f → ⁅h, e⁆ = 2 • e
Defined in
Mathlib.Algebra.Lie.Sl2
Cited by
4 results in Mathlib
Foundations
Depth 8 from the axioms · uses no axioms
Assumes
LieRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

IsSl2Triple.lie_h_e_smul · cited by 2IsSl2Triple.lie_h_e_smulIsSl2Triple.symm · cited by 2IsSl2Triple.symmLieAlgebra.Basis.A_diag_eq_two · cited by 1Basis.A_diag_eq_twoIsSl2Triple.HasPrimitiveVectorWith.mk' · cited by 0HasPrimitiveVectorWith.mk'LieRing · cited by 1548LieRingBracket.bracket · cited by 642Bracket.bracketIsSl2Triple · cited by 38IsSl2TripleIsSl2Triple.lie_h_e_nsmulCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by4

Results whose statement or proof uses this declaration.